Perfect pairings #

This file defines 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 reflexive modules.
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

Instances

source

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

source

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

source

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 Mand N, we may interchange the roles of M and N.

source

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 Mand N, we may interchange the roles of M and N.

source

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.

Equations

p.toPerfPair = LinearEquiv.ofBijective { toFun := p.1.toFun, map_add' := ⋯, map_smul' := ⋯ } ⋯

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

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.

source

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.

source

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

source

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

source

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

source

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.

source

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.

source

@[deprecated LinearMap.IsPerfPair (since := "2025-05-27")]

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.

toFun : M → N →ₗ[R] R
map_add' (x y : M) : self.toFun (x + y) = self.toFun x + self.toFun y
map_smul' (m : R) (x : M) : self.toFun (m • x) = (RingHom.id R) m • self.toFun x
bijective_left : Function.Bijective ⇑self.toLinearMap
bijective_right : Function.Bijective ⇑self.flip

Instances For

source

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

M →ₗ[R] N →ₗ[R] R

Alias of PerfectPairing.toLinearMap.

The underlying bilinear map of a perfect pairing.

Equations

@PerfectPairing.toLin = @PerfectPairing.toLinearMap

Instances For

source

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

Function.Bijective ⇑self.toLinearMap

Alias of PerfectPairing.bijective_left.

source

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

Function.Bijective ⇑self.flip

Alias of PerfectPairing.bijective_right.

source

@[deprecated LinearMap.IsPerfPair.of_injective (since := "2025-05-27")]

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

PerfectPairing K V W

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' = { toLinearMap := B, bijective_left := ⋯, bijective_right := ⋯ }

Instances For

source

@[deprecated LinearMap.IsPerfPair.of_injective' (since := "2025-05-27")]

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

PerfectPairing K V W

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' = { toLinearMap := B, bijective_left := ⋯, bijective_right := ⋯ }

Instances For

source

@[deprecated "No replacement" (since := "2025-05-27")]

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

FunLike (PerfectPairing R M N) M (N →ₗ[R] R)

Equations

PerfectPairing.instFunLike = { coe := fun (f : PerfectPairing R M N) => ⇑f.toLinearMap, coe_injective' := ⋯ }

source

@[deprecated "No replacement" (since := "2025-05-27")]

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

source

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

source

@[deprecated "No replacement" (since := "2025-05-27")]

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

source

@[deprecated LinearMap.IsPerfPair.flip (since := "2025-05-27")]

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

PerfectPairing R N M

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 := ⋯ }

Instances For

source

@[deprecated "No replacement" (since := "2025-05-27")]

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

source

@[deprecated "No replacement" (since := "2025-05-27")]

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

source

@[deprecated LinearMap.toPerfPair (since := "2025-05-27")]

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

M ≃ₗ[R] Module.Dual R N

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

Equations

p.toDualLeft = LinearEquiv.ofBijective p.toLinearMap ⋯

Instances For

source

@[deprecated "No replacement" (since := "2025-05-27")]

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

source

@[deprecated "No replacement" (since := "2025-05-27")]

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

source

@[deprecated LinearMap.toPerfPair (since := "2025-05-27")]

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

N ≃ₗ[R] Module.Dual R M

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

Equations

p.toDualRight = p.flip.toDualLeft

Instances For

source

@[deprecated "No replacement" (since := "2025-05-27")]

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

p.toDualRight a = p.flip a

source

@[deprecated "No replacement" (since := "2025-05-27")]

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

source

@[deprecated "No replacement" (since := "2025-05-27")]

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

source

@[deprecated "No replacement" (since := "2025-05-27")]

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

p.toDualRight.symm.dualMap (p.toDualLeft x) = (Module.Dual.eval R M) x

source

@[deprecated "No replacement" (since := "2025-05-27")]

theorem PerfectPairing.toDualRight_symm_comp_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) :

↑p.toDualRight.symm.dualMap ∘ₗ ↑p.toDualLeft = Module.Dual.eval R M

source

@[deprecated "No replacement" (since := "2025-05-27")]

theorem PerfectPairing.bijective_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) :

Function.Bijective fun (x : M) => p.toDualRight.symm.dualMap (p.toDualLeft x)

source

@[deprecated Module.IsReflexive.of_isPerfPair (since := "2025-05-27")]

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

Module.IsReflexive R M

source

@[deprecated Module.IsReflexive.of_isPerfPair (since := "2025-05-27")]

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

Module.IsReflexive R N

source

@[deprecated "No replacement" (since := "2025-05-27")]

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

EquivLike (PerfectPairing R M N) M (Module.Dual R N)

Equations

One or more equations did not get rendered due to their size.

source

@[deprecated "No replacement" (since := "2025-05-27")]

instance PerfectPairing.instLinearEquivClassDual {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] :

LinearEquivClass (PerfectPairing R M N) R M (Module.Dual R N)

source

@[deprecated Module.finrank_of_isPerfPair (since := "2025-05-27")]

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

Module.finrank R M = Module.finrank R N

source

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

Instances For

source

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

source

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

source

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

source

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

source

@[deprecated LinearMap.IsPerfPair.id (since := "2025-05-27")]

def IsReflexive.toPerfectPairingDual {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] :

PerfectPairing R (Module.Dual R M) M

A reflexive module has a perfect pairing with its dual.

Equations

IsReflexive.toPerfectPairingDual = { toLinearMap := LinearMap.id, bijective_left := ⋯, bijective_right := ⋯ }

Instances For

source

@[deprecated "No replacement" (since := "2025-05-27")]

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

(toPerfectPairingDual f) x = f x

source

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.

Equations

e.flip = (Module.evalEquiv R M).trans e.dualMap

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

↑e.flip = (↑e).flip

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

(e.flip m) n = (e n) m

source

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

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

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

e.flip.flip = e

source

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

source

@[deprecated "No replacement" (since := "2025-05-27")]

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

PerfectPairing R N M

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

Equations

e.toPerfectPairing = { toLinearMap := ↑e, bijective_left := ⋯, bijective_right := ⋯ }

Instances For

source

@[deprecated "No replacement" (since := "2025-05-27")]

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

PerfectPairing R (Module.Dual R M) (Module.Dual R N)

A perfect pairing induces a perfect pairing between dual spaces.

Equations

p.dual = (p.toDualRight.symm.trans (Module.evalEquiv R N)).toPerfectPairing

Instances For

source

@[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] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M) (p : Submodule R M) :

(map e.flip p).dualCoannihilator = map e.symm p.dualAnnihilator

source

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

source

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

source

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

Documentation

Mathlib.LinearAlgebra.PerfectPairing.Basic

Perfect pairings #