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 mapsM → Dual R N
andN → Dual R M
are both bijective. It follows from this that bothM
andN
are reflexive modules. - A linear equivalence
N ≃ Dual R M
for whichM
is reflexive. (It then follows thatN
is reflexive.)
In this file we provide a PerfectPairing
definition corresponding to 1 above, together with logic
to connect 1 and 2.
Main definitions #
A perfect pairing of two (left) modules over a commutative ring.
- bijectiveLeft : Function.Bijective ⇑self.toLin
- bijectiveRight : Function.Bijective ⇑self.toLin.flip
Instances For
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
- PerfectPairing.mkOfInjective B h h' = { toLin := B, bijectiveLeft := ⋯, bijectiveRight := ⋯ }
Instances For
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
- PerfectPairing.mkOfInjective' B h h' = { toLin := B, bijectiveLeft := ⋯, bijectiveRight := ⋯ }
Instances For
Equations
- PerfectPairing.instFunLike = { coe := fun (f : PerfectPairing R M N) => ⇑f.toLin, coe_injective' := ⋯ }
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
The linear equivalence from M
to Dual R N
induced by a perfect pairing.
Equations
- p.toDualLeft = LinearEquiv.ofBijective p.toLin ⋯
Instances For
The linear equivalence from N
to Dual R M
induced by a perfect pairing.
Equations
- p.toDualRight = p.flip.toDualLeft
Instances For
Equations
- One or more equations did not get rendered due to their size.
The restriction of a perfect pairing to submodules (expressed as injections to provide definitional control).
Equations
- p.restrict i j hM hN hi hj = { toLin := p.toLin.compl₁₂ i j, bijectiveLeft := ⋯, bijectiveRight := ⋯ }
Instances For
If a perfect pairing over a field L
takes values in a subfield K
along two K
-subspaces
whose L
span is full, then these subspaces induce a K
-structure in the sense of
Algebra I, Bourbaki : Chapter II, §8.1 Definition 1.
Restriction of scalars for a perfect pairing taking values in a subring.
Equations
- p.restrictScalars i j hi hj hM hN h₁ h₂ hp = { toLin := PerfectPairing.restrictScalarsAux✝ p i j hp, bijectiveLeft := ⋯, bijectiveRight := ⋯ }
Instances For
Restriction of scalars for a perfect pairing taking values in a subfield.
Equations
- PerfectPairing.restrictScalarsField i j hi hj hM hN p hp = PerfectPairing.mkOfInjective (PerfectPairing.restrictScalarsAux✝ p i j hp) ⋯ ⋯
Instances For
A reflexive module has a perfect pairing with its dual.
Equations
- IsReflexive.toPerfectPairingDual = { toLin := LinearMap.id, bijectiveLeft := ⋯, bijectiveRight := ⋯ }
Instances For
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 = (Module.evalEquiv R M).trans e.dualMap
Instances For
If N
is in perfect pairing with M
, then it is reflexive.
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
A perfect pairing induces a perfect pairing between dual spaces.
Equations
- p.dual = (p.toDualRight.symm.trans (Module.evalEquiv R N)).toPerfectPairing