Perfect pairings

This file defines 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 definition IsPerfPair corresponding to 1 above, together with logic to connect 1 and 2.

class LinearMap.IsPerfPair {R : Type u_1} {M : Type u_3} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) : Prop

For a ring R and two modules M and N, a perfect pairing is a bilinear map M × N → R that is bijective in both arguments.

• bijective_left : Function.Bijective ⇑p
• bijective_right : Function.Bijective ⇑p.flip

theorem LinearMap.IsPerfPair.ext {R : Type u_1} {M : Type u_3} {N : Type u_5} {inst✝ : AddCommGroup M} {inst✝¹ : AddCommGroup N} {inst✝² : CommRing R} {inst✝³ : Module R M} {inst✝⁴ : Module R N} {p : M →ₗ[R] N →ₗ[R] R} {x y : p.IsPerfPair} : x = y

theorem LinearMap.IsPerfPair.ext_iff {R : Type u_1} {M : Type u_3} {N : Type u_5} {inst✝ : AddCommGroup M} {inst✝¹ : AddCommGroup N} {inst✝² : CommRing R} {inst✝³ : Module R M} {inst✝⁴ : Module R N} {p : M →ₗ[R] N →ₗ[R] R} {x y : p.IsPerfPair} : x = y ↔ True

theorem LinearMap.IsPerfPair.flip {R : Type u_1} {M : Type u_3} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} (hp : p.IsPerfPair) : p.flip.IsPerfPair

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

instance LinearMap.flip.instIsPerfPair {R : Type u_1} {M : Type u_3} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} [p.IsPerfPair] : p.flip.IsPerfPair

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

noncomputable def LinearMap.toPerfPair {R : Type u_1} {M : Type u_3} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] : M ≃ₗ[R] Module.Dual R N

Turn a perfect pairing between M and N into an isomorphism between M and the dual of N.

@[simp]

theorem LinearMap.toLinearMap_toPerfPair {R : Type u_1} {M : Type u_3} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] (x : M) : p.toPerfPair x = p x

@[simp]

theorem LinearMap.toPerfPair_apply {R : Type u_1} {M : Type u_3} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] (x : M) (y : N) : (p.toPerfPair x) y = (p x) y

@[simp]

theorem LinearMap.apply_symm_toPerfPair_self {R : Type u_1} {M : Type u_3} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] (f : Module.Dual R N) : p (p.toPerfPair.symm f) = f

@[simp]

theorem LinearMap.apply_toPerfPair_flip {R : Type u_1} {M : Type u_3} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] (f : Module.Dual R M) (x : M) : (p x) (p.flip.toPerfPair.symm f) = f x

theorem Module.IsReflexive.of_isPerfPair {R : Type u_1} {M : Type u_3} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] : IsReflexive R M

theorem Module.finrank_of_isPerfPair {R : Type u_1} {M : Type u_3} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] [Module.Finite R M] [Free R M] : finrank R M = finrank R N

instance LinearMap.IsPerfPair.id {R : Type u_1} {M : Type u_3} [AddCommGroup M] [CommRing R] [Module R M] [Module.IsReflexive R M] : id.IsPerfPair

A reflexive module has a perfect pairing with its dual.

instance LinearMap.IsPerfPair.dualEval {R : Type u_1} {M : Type u_3} [AddCommGroup M] [CommRing R] [Module R M] [Module.IsReflexive R M] : (Module.Dual.eval R M).IsPerfPair

A reflexive module has a perfect pairing with its dual.

instance LinearMap.IsPerfPair.compl₁₂ {R : Type u_1} {M : Type u_3} {M' : Type u_4} {N : Type u_5} {N' : Type u_6} [AddCommGroup M] [AddCommGroup N] [AddCommGroup M'] [AddCommGroup N'] [CommRing R] [Module R M] [Module R M'] [Module R N] [Module R N'] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] (eM : M' ≃ₗ[R] M) (eN : N' ≃ₗ[R] N) : (p.compl₁₂ ↑eM ↑eN).IsPerfPair

theorem LinearMap.IsPerfPair.congr {R : Type u_1} {M : Type u_3} {M' : Type u_4} {N : Type u_5} {N' : Type u_6} [AddCommGroup M] [AddCommGroup N] [AddCommGroup M'] [AddCommGroup N'] [CommRing R] [Module R M] [Module R M'] [Module R N] [Module R N'] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] (eM : M' ≃ₗ[R] M) (eN : N' ≃ₗ[R] N) (q : M' →ₗ[R] N' →ₗ[R] R) (H : q.compl₁₂ ↑eM.symm ↑eN.symm = p) : q.IsPerfPair

theorem LinearMap.IsPerfPair.of_bijective {R : Type u_1} {M : Type u_3} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) [Module.IsReflexive R N] (h : Function.Bijective ⇑p) : p.IsPerfPair

theorem LinearMap.IsPerfPair.of_injective {K : Type u_2} {M : Type u_3} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] [Field K] [Module K M] [Module K N] {p : M →ₗ[K] N →ₗ[K] K} [FiniteDimensional K M] (h : Function.Injective ⇑p) (h' : Function.Injective ⇑p.flip) : p.IsPerfPair

If the coefficients are a field, and one of the spaces is finite-dimensional, it is sufficient to check only injectivity instead of bijectivity of the bilinear pairing.

theorem LinearMap.IsPerfPair.of_injective' {K : Type u_2} {M : Type u_3} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] [Field K] [Module K M] [Module K N] {p : M →ₗ[K] N →ₗ[K] K} [FiniteDimensional K N] (h : Function.Injective ⇑p) (h' : Function.Injective ⇑p.flip) : p.IsPerfPair

If the coefficients are a field, and one of the spaces is finite-dimensional, it is sufficient to check only injectivity instead of bijectivity of the bilinear pairing.

structure LinearMap.IsPerfectCompl {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 : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] (U : Submodule R M) (V : Submodule R N) : Prop

Given a perfect pairing p between M and N, we say a pair of submodules U in M and V in N are perfectly complementary w.r.t. p if their dual annihilators are complementary, using p to identify M and N with dual spaces.

• isCompl_left : IsCompl U (Submodule.map (↑p.toPerfPair.symm) V.dualAnnihilator)
• isCompl_right : IsCompl V (Submodule.map (↑p.flip.toPerfPair.symm) U.dualAnnihilator)

theorem LinearMap.IsPerfectCompl.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 : M →ₗ[R] N →ₗ[R] R} [p.IsPerfPair] {U : Submodule R M} {V : Submodule R N} (h : p.IsPerfectCompl U V) : p.flip.IsPerfectCompl V U

@[simp]

theorem LinearMap.IsPerfectCompl.flip_iff {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 : M →ₗ[R] N →ₗ[R] R} [p.IsPerfPair] {U : Submodule R M} {V : Submodule R N} : p.flip.IsPerfectCompl V U ↔ p.IsPerfectCompl U V

@[simp]

theorem LinearMap.IsPerfectCompl.left_top_iff {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 : M →ₗ[R] N →ₗ[R] R} [p.IsPerfPair] {V : Submodule R N} : p.IsPerfectCompl ⊤ V ↔ V = ⊤

@[simp]

theorem LinearMap.IsPerfectCompl.right_top_iff {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 : M →ₗ[R] N →ₗ[R] R} [p.IsPerfPair] {U : Submodule R M} : p.IsPerfectCompl U ⊤ ↔ U = ⊤

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.

@[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) : ↑e.flip = (↑e).flip

@[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) : (e.flip 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) : e.flip.symm = e.symm.dualMap ≪≫ₗ (Module.evalEquiv R M).symm

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 ≪≫ₗ e.flip.symm.dualMap) = 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 : Module.IsReflexive R N := ⋯) : e.flip.flip = e

instance LinearEquiv.instIsPerfPair {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).IsPerfPair

@[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] (e : N ≃ₗ[R] Module.Dual R M) (p : Submodule R M) : (map (↑e).flip p).dualCoannihilator = 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} [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) : map (↑e.flip.symm) p.dualAnnihilator = (map (↑e) p).dualCoannihilator

@[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)) : map (↑e).flip p.dualCoannihilator = (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} [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)) : (map (↑e.flip.symm) p).dualAnnihilator = map (↑e) p.dualCoannihilator