Perfect pairings of modules

A perfect pairing of two (left) modules may be defined either as:

1. A bilinear map M × N → R such that the induced maps M → Dual R N and N → Dual R M are both bijective. (It follows from this that both M and N are both reflexive modules.)
2. A linear equivalence N ≃ Dual R M for which M is reflexive. (It then follows that N is reflexive.)

In this file we provide a PerfectPairing definition corresponding to 1 above, together with logic to connect 1 and 2.

Main definitions

• PerfectPairing
• PerfectPairing.flip
• LinearEquiv.flip
• LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive
• LinearEquiv.toPerfectPairing

structure PerfectPairing (R : Type u_1) (M : Type u_2) (N : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : Type (max (max u_1 u_2) u_3)

A perfect pairing of two (left) modules over a commutative ring.

• toLin : M →ₗ[R] N →ₗ[R] R
• bijectiveLeft : Function.Bijective ⇑self.toLin
• bijectiveRight : Function.Bijective ⇑(LinearMap.flip self.toLin)

instance PerfectPairing.instFunLike {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : FunLike (PerfectPairing R M N) M (N →ₗ[R] R)

Equations

• PerfectPairing.instFunLike = { coe := fun (f : PerfectPairing R M N) => ⇑f.toLin, coe_injective' := ⋯ }

def PerfectPairing.flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) : PerfectPairing R N M

Given a perfect pairing between M and N, we may interchange the roles of M and N.

Equations

• PerfectPairing.flip p = { toLin := LinearMap.flip p.toLin, bijectiveLeft := ⋯, bijectiveRight := ⋯ }

@[simp]

theorem PerfectPairing.flip_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) : PerfectPairing.flip (PerfectPairing.flip p) = p

@[simp]

theorem IsReflexive.toPerfectPairingDual_toLin {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] : IsReflexive.toPerfectPairingDual.toLin = LinearMap.id

def IsReflexive.toPerfectPairingDual {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] : PerfectPairing R (Module.Dual R M) M

A reflexive module has a perfect pairing with its dual.

Equations

• IsReflexive.toPerfectPairingDual = { toLin := LinearMap.id, bijectiveLeft := ⋯, bijectiveRight := ⋯ }

noncomputable def LinearEquiv.flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) : M ≃ₗ[R] Module.Dual R N

For a reflexive module M, an equivalence N ≃ₗ[R] Dual R M naturally yields an equivalence M ≃ₗ[R] Dual R N. Such equivalences are known as perfect pairings.

Equations

• LinearEquiv.flip e = LinearEquiv.trans (Module.evalEquiv R M) (LinearEquiv.dualMap e)

@[simp]

theorem LinearEquiv.coe_toLinearMap_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) : ↑(LinearEquiv.flip e) = LinearMap.flip ↑e

@[simp]

theorem LinearEquiv.flip_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) (m : M) (n : N) : ((LinearEquiv.flip e) m) n = (e n) m

theorem LinearEquiv.symm_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) : LinearEquiv.symm (LinearEquiv.flip e) = LinearEquiv.dualMap (LinearEquiv.symm e) ≪≫ₗ LinearEquiv.symm (Module.evalEquiv R M)

theorem LinearEquiv.trans_dualMap_symm_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) : ↑(e ≪≫ₗ LinearEquiv.dualMap (LinearEquiv.symm (LinearEquiv.flip e))) = Module.Dual.eval R N

theorem LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) : Module.IsReflexive R N

If N is in perfect pairing with M, then it is reflexive.

@[simp]

theorem LinearEquiv.flip_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) (h : optParam (Module.IsReflexive R N) ⋯) : LinearEquiv.flip (LinearEquiv.flip e) = e

@[simp]

theorem LinearEquiv.toPerfectPairing_toLin {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) : (LinearEquiv.toPerfectPairing e).toLin = ↑e

noncomputable def LinearEquiv.toPerfectPairing {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) : PerfectPairing R N M

If M is reflexive then a linear equivalence N ≃ Dual R M is a perfect pairing.

Equations

• LinearEquiv.toPerfectPairing e = { toLin := ↑e, bijectiveLeft := ⋯, bijectiveRight := ⋯ }

@[simp]

theorem Submodule.dualCoannihilator_map_linearEquiv_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) (p : Submodule R M) : Submodule.dualCoannihilator (Submodule.map (LinearEquiv.flip e) p) = Submodule.map (LinearEquiv.symm e) (Submodule.dualAnnihilator p)

@[simp]

theorem Submodule.map_dualAnnihilator_linearEquiv_flip_symm {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) (p : Submodule R N) : Submodule.map (LinearEquiv.symm (LinearEquiv.flip e)) (Submodule.dualAnnihilator p) = Submodule.dualCoannihilator (Submodule.map e p)

@[simp]

theorem Submodule.map_dualCoannihilator_linearEquiv_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) (p : Submodule R (Module.Dual R M)) : Submodule.map (LinearEquiv.flip e) (Submodule.dualCoannihilator p) = Submodule.dualAnnihilator (Submodule.map (LinearEquiv.symm e) p)

@[simp]

theorem Submodule.dualAnnihilator_map_linearEquiv_flip_symm {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) (p : Submodule R (Module.Dual R N)) : Submodule.dualAnnihilator (Submodule.map (LinearEquiv.symm (LinearEquiv.flip e)) p) = Submodule.map e (Submodule.dualCoannihilator p)