# 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 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
• PerfectPairing.toDualLeft
• PerfectPairing.toDualRight
• 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) [] [] [Module R M] [] [Module R N] :
Type (max (max u_1 u_2) u_3)

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

Instances For
theorem PerfectPairing.bijectiveLeft {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (self : ) :
Function.Bijective self.toLin
theorem PerfectPairing.bijectiveRight {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (self : ) :
Function.Bijective self.toLin.flip
instance PerfectPairing.instFunLike {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] :
FunLike () M (N →ₗ[R] R)
Equations
• PerfectPairing.instFunLike = { coe := fun (f : ) => f.toLin, coe_injective' := }
def PerfectPairing.flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (p : ) :

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

Equations
• p.flip = { toLin := p.toLin.flip, bijectiveLeft := , bijectiveRight := }
Instances For
@[simp]
theorem PerfectPairing.flip_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (p : ) :
p.flip.flip = p
noncomputable def PerfectPairing.toDualLeft {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (p : ) :

The linear equivalence from M to Dual R N induced by a perfect pairing.

Equations
Instances For
@[simp]
theorem PerfectPairing.toDualLeft_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (p : ) (a : M) :
p.toDualLeft a = p a
@[simp]
theorem PerfectPairing.apply_toDualLeft_symm_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (p : ) (f : ) (x : N) :
(p (p.toDualLeft.symm f)) x = f x
noncomputable def PerfectPairing.toDualRight {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (p : ) :

The linear equivalence from N to Dual R M induced by a perfect pairing.

Equations
• p.toDualRight = p.flip.toDualLeft
Instances For
@[simp]
theorem PerfectPairing.toDualRight_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (p : ) (a : N) :
p.toDualRight a = p.flip a
@[simp]
theorem PerfectPairing.apply_apply_toDualRight_symm {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (p : ) (x : M) (f : ) :
(p x) (p.toDualRight.symm f) = f x
theorem PerfectPairing.toDualLeft_of_toDualRight_symm {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (p : ) (x : M) (f : ) :
(p.toDualLeft x) (p.toDualRight.symm f) = f x
theorem PerfectPairing.toDualRight_symm_toDualLeft {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (p : ) (x : M) :
p.toDualRight.symm.dualMap (p.toDualLeft x) = () x
theorem PerfectPairing.toDualRight_symm_comp_toDualLeft {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (p : ) :
p.toDualRight.symm.dualMap ∘ₗ p.toDualLeft =
theorem PerfectPairing.bijective_toDualRight_symm_toDualLeft {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (p : ) :
Function.Bijective fun (x : M) => p.toDualRight.symm.dualMap (p.toDualLeft x)
theorem PerfectPairing.reflexive_left {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (p : ) :
theorem PerfectPairing.reflexive_right {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] (p : ) :
@[simp]
theorem IsReflexive.toPerfectPairingDual_toLin {R : Type u_1} {M : Type u_2} [] [] [Module R M] [] :
IsReflexive.toPerfectPairingDual.toLin = LinearMap.id
def IsReflexive.toPerfectPairingDual {R : Type u_1} {M : Type u_2} [] [] [Module R M] [] :

A reflexive module has a perfect pairing with its dual.

Equations
• IsReflexive.toPerfectPairingDual = { toLin := LinearMap.id, bijectiveLeft := , bijectiveRight := }
Instances For
noncomputable def LinearEquiv.flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] [] (e : N ≃ₗ[R] ) :

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
• e.flip = ().trans e.dualMap
Instances For
@[simp]
theorem LinearEquiv.coe_toLinearMap_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] [] (e : N ≃ₗ[R] ) :
e.flip = e.flip
@[simp]
theorem LinearEquiv.flip_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] [] (e : N ≃ₗ[R] ) (m : M) (n : N) :
(e.flip m) n = (e n) m
theorem LinearEquiv.symm_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] [] (e : N ≃ₗ[R] ) :
e.flip.symm = e.symm.dualMap ≪≫ₗ ().symm
theorem LinearEquiv.trans_dualMap_symm_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] [] (e : N ≃ₗ[R] ) :
(e ≪≫ₗ e.flip.symm.dualMap) =
theorem LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] [] (e : N ≃ₗ[R] ) :

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} [] [] [Module R M] [] [Module R N] [] (e : N ≃ₗ[R] ) (h : optParam () ) :
e.flip.flip = e
@[simp]
theorem LinearEquiv.toPerfectPairing_toLin {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] [] (e : N ≃ₗ[R] ) :
e.toPerfectPairing.toLin = e
noncomputable def LinearEquiv.toPerfectPairing {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] [] (e : N ≃ₗ[R] ) :

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

Equations
• e.toPerfectPairing = { toLin := e, bijectiveLeft := , bijectiveRight := }
Instances For
@[simp]
theorem Submodule.dualCoannihilator_map_linearEquiv_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] [] (e : N ≃ₗ[R] ) (p : ) :
(Submodule.map e.flip p).dualCoannihilator = Submodule.map e.symm p.dualAnnihilator
@[simp]
theorem Submodule.map_dualAnnihilator_linearEquiv_flip_symm {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] [] (e : N ≃ₗ[R] ) (p : ) :
Submodule.map e.flip.symm p.dualAnnihilator = ().dualCoannihilator
@[simp]
theorem Submodule.map_dualCoannihilator_linearEquiv_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] [] (e : N ≃ₗ[R] ) (p : Submodule R ()) :
Submodule.map e.flip p.dualCoannihilator = (Submodule.map e.symm p).dualAnnihilator
@[simp]
theorem Submodule.dualAnnihilator_map_linearEquiv_flip_symm {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [Module R N] [] (e : N ≃ₗ[R] ) (p : Submodule R ()) :
(Submodule.map e.flip.symm p).dualAnnihilator = Submodule.map e p.dualCoannihilator