Perfect pairings of modules #

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

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.)
A linear equivalence N ≃ Dual R M for which M is reflexive. (It then follows that N is reflexive.)

The second definition is more convenient and we prove some basic facts about it here.

Main definitions #

LinearEquiv.flip
LinearEquiv.IsReflexive_of_equiv_Dual_of_IsReflexive

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.

Instances For

source

@[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

source

@[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

source

@[simp]

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.trans (LinearEquiv.dualMap (LinearEquiv.symm e)) (LinearEquiv.symm (Module.evalEquiv R M))

source

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) :

↑(LinearEquiv.trans e (LinearEquiv.dualMap (LinearEquiv.symm (LinearEquiv.flip e)))) = Module.Dual.eval R N

source

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.

source

@[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) (_ : Module.IsReflexive R N)) :

LinearEquiv.flip (LinearEquiv.flip e) = e