Documentation

Mathlib.LinearAlgebra.PerfectPairing.Basic

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 #

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] extends M →ₗ[R] N →ₗ[R] R :
Type (max (max u_1 u_2) u_3)

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

@[deprecated PerfectPairing.toLinearMap (since := "2025-04-20")]
def PerfectPairing.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] (self : PerfectPairing R M N) :

Alias of PerfectPairing.toLinearMap.


The underlying bilinear map of a perfect pairing.

Equations
@[deprecated PerfectPairing.bijective_left (since := "2025-04-20")]
theorem PerfectPairing.bijectiveLeft {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (self : PerfectPairing R M N) :

Alias of PerfectPairing.bijective_left.

@[deprecated PerfectPairing.bijective_right (since := "2025-04-20")]
theorem PerfectPairing.bijectiveRight {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (self : PerfectPairing R M N) :

Alias of PerfectPairing.bijective_right.

def PerfectPairing.mkOfInjective {K : Type u_4} {V : Type u_5} {W : Type u_6} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K V] (B : V →ₗ[K] W →ₗ[K] K) (h : Function.Injective B) (h' : Function.Injective B.flip) :

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 form.

Equations
def PerfectPairing.mkOfInjective' {K : Type u_4} {V : Type u_5} {W : Type u_6} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] (B : V →ₗ[K] W →ₗ[K] K) (h : Function.Injective B) (h' : Function.Injective B.flip) :

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 form.

Equations
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] :
Equations
@[simp]
theorem PerfectPairing.toLinearMap_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] (p : PerfectPairing R M N) (x : M) :
p.toLinearMap x = p x
@[deprecated PerfectPairing.toLinearMap_apply (since := "2025-04-20")]
theorem PerfectPairing.toLin_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] (p : PerfectPairing R M N) (x : M) :
p.toLinearMap x = p x

Alias of PerfectPairing.toLinearMap_apply.

@[simp]
theorem PerfectPairing.mk_apply_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] {f : M →ₗ[R] N →ₗ[R] R} {hl : Function.Bijective f} {hr : Function.Bijective f.flip} {x : M} :
{ toLinearMap := f, bijective_left := hl, bijective_right := hr } x = f x
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) :

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

Equations
  • p.flip = { toLinearMap := p.flip, bijective_left := , bijective_right := }
@[simp]
theorem PerfectPairing.flip_apply_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] (p : PerfectPairing R M N) {x : M} {y : N} :
(p.flip y) x = (p x) y
@[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) :
p.flip.flip = p
def PerfectPairing.toDualLeft {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) :

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

Equations
@[simp]
theorem PerfectPairing.toDualLeft_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] (p : PerfectPairing R M N) (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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) (f : Module.Dual R N) (x : N) :
(p (p.toDualLeft.symm f)) x = f x
def PerfectPairing.toDualRight {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) :

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

Equations
@[simp]
theorem PerfectPairing.toDualRight_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] (p : PerfectPairing R M N) (a : N) :
@[simp]
theorem PerfectPairing.apply_apply_toDualRight_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] (p : PerfectPairing R M N) (x : M) (f : Module.Dual R M) :
(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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) (x : M) (f : Module.Dual R M) :
(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} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : PerfectPairing R M N) (x : M) :
theorem PerfectPairing.reflexive_left {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) :
theorem PerfectPairing.reflexive_right {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) :
instance PerfectPairing.instEquivLikeDual {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] :
Equations
  • One or more equations did not get rendered due to their size.
theorem PerfectPairing.finrank_eq {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) [Module.Finite R M] [Module.Free R M] :
structure PerfectPairing.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 : PerfectPairing R M N) (U : Submodule R M) (V : Submodule R N) :

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 wrt p if their dual annihilators are complementary, using p to identify M and N with dual spaces.

theorem PerfectPairing.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 : PerfectPairing R M N} {U : Submodule R M} {V : Submodule R N} (h : p.IsPerfectCompl U V) :
@[simp]
theorem PerfectPairing.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 : PerfectPairing R M N} {U : Submodule R M} {V : Submodule R N} :
@[simp]
theorem PerfectPairing.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 : PerfectPairing R M N} {V : Submodule R N} :
@[simp]
theorem PerfectPairing.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 : PerfectPairing R M N} {U : Submodule R M} :

A reflexive module has a perfect pairing with its dual.

Equations
@[simp]
theorem IsReflexive.toPerfectPairingDual_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] {f : Module.Dual R M} {x : M} :
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) :

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

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

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

Equations
def PerfectPairing.dual {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) :

A perfect pairing induces a perfect pairing between dual spaces.

Equations