Restriction to submodules and restriction of scalars for perfect pairings.

We provide API for restricting perfect pairings to submodules and for restricting their scalars.

Main definitions

• PerfectPairing.restrict: restriction of a perfect pairing to submodules.
• PerfectPairing.restrictScalars: restriction of scalars for a perfect pairing taking values in a subring.
• PerfectPairing.restrictScalarsField: simultaneously restrict both the domains and scalars of a perfect pairing with coefficients in a field.

theorem LinearMap.IsPerfPair.restrict {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] {M' : Type u_4} {N' : Type u_5} [AddCommGroup M'] [Module R M'] [AddCommGroup N'] [Module R N'] (i : M' →ₗ[R] M) (j : N' →ₗ[R] N) (hi : Function.Injective ⇑i) (hj : Function.Injective ⇑j) (hij : p.IsPerfectCompl (range i) (range j)) : (p.compl₁₂ i j).IsPerfPair

The restriction of a perfect pairing to submodules is a perfect pairing.

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

def PerfectPairing.restrict {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] {M' : Type u_4} {N' : Type u_5} [AddCommGroup M'] [Module R M'] [AddCommGroup N'] [Module R N'] (i : M' →ₗ[R] M) (j : N' →ₗ[R] N) (hi : Function.Injective ⇑i) (hj : Function.Injective ⇑j) (hij : p.IsPerfectCompl (LinearMap.range i) (LinearMap.range j)) : PerfectPairing R M' N'

The restriction of a perfect pairing to submodules (expressed as injections to provide definitional control).

Equations

• PerfectPairing.restrict p i j hi hj hij = { toLinearMap := p.compl₁₂ i j, bijective_left := ⋯, bijective_right := ⋯ }

theorem LinearMap.IsPerfPair.restrictScalars {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] {S : Type u_4} {M' : Type u_5} {N' : Type u_6} [CommRing S] [Algebra S R] [Module S M] [Module S N] [IsScalarTower S R M] [IsScalarTower S R N] [NoZeroSMulDivisors S R] [Nontrivial R] [AddCommGroup M'] [Module S M'] [AddCommGroup N'] [Module S N'] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N) (hi : Function.Injective ⇑i) (hj : Function.Injective ⇑j) (hM : Submodule.span R ↑(range i) = ⊤) (hN : Submodule.span R ↑(range j) = ⊤) (h₁ : ∀ (g : Module.Dual S N'), ∃ (m : M'), ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g) (h₂ : ∀ (g : Module.Dual S M'), ∃ (n : N'), ↑S (p.flip.toPerfPair (j n)) ∘ₗ i = Algebra.linearMap S R ∘ₗ g) (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range) : (i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp).IsPerfPair

Restricting a perfect pairing to a subring of the scalars results in a perfect pairing.

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

def PerfectPairing.restrictScalars {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] {S : Type u_4} {M' : Type u_5} {N' : Type u_6} [CommRing S] [Algebra S R] [Module S M] [Module S N] [IsScalarTower S R M] [IsScalarTower S R N] [NoZeroSMulDivisors S R] [Nontrivial R] [AddCommGroup M'] [Module S M'] [AddCommGroup N'] [Module S N'] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N) (hi : Function.Injective ⇑i) (hj : Function.Injective ⇑j) (hM : Submodule.span R ↑(LinearMap.range i) = ⊤) (hN : Submodule.span R ↑(LinearMap.range j) = ⊤) (h₁ : ∀ (g : Module.Dual S N'), ∃ (m : M'), ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g) (h₂ : ∀ (g : Module.Dual S M'), ∃ (n : N'), ↑S (p.flip.toPerfPair (j n)) ∘ₗ i = Algebra.linearMap S R ∘ₗ g) (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range) : PerfectPairing S M' N'

Restriction of scalars for a perfect pairing taking values in a subring.

Equations

• PerfectPairing.restrictScalars p i j hi hj hM hN h₁ h₂ hp = { toLinearMap := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp, bijective_left := ⋯, bijective_right := ⋯ }

theorem LinearMap.exists_basis_basis_of_span_eq_top_of_mem_algebraMap {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field K] [Field L] [Algebra K L] [AddCommGroup M] [AddCommGroup N] [Module L M] [Module L N] [Module K M] [Module K N] [IsScalarTower K L M] (p : M →ₗ[L] N →ₗ[L] L) [p.IsPerfPair] (M' : Submodule K M) (N' : Submodule K N) (hM : Submodule.span L ↑M' = ⊤) (hN : Submodule.span L ↑N' = ⊤) (hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range) : ∃ (n : ℕ) (b : Module.Basis (Fin n) L M) (b' : Module.Basis (Fin n) K ↥M'), ∀ (i : Fin n), b i = ↑(b' i)

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.

theorem LinearMap.IsPerfPair.restrictScalars_of_field {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field K] [Field L] [Algebra K L] [AddCommGroup M] [AddCommGroup N] [Module L M] [Module L N] [Module K M] [Module K N] [IsScalarTower K L M] (p : M →ₗ[L] N →ₗ[L] L) [p.IsPerfPair] {M' : Type u_5} {N' : Type u_6} [AddCommGroup M'] [AddCommGroup N'] [Module K M'] [Module K N'] [IsScalarTower K L N] (i : M' →ₗ[K] M) (j : N' →ₗ[K] N) (hi : Function.Injective ⇑i) (hj : Function.Injective ⇑j) (hij : p.IsPerfectCompl (Submodule.span L ↑(range i)) (Submodule.span L ↑(range j))) (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range) : (i.restrictScalarsRange₂ j (Algebra.linearMap K L) ⋯ p hp).IsPerfPair

Simultaneously restrict both the domains and scalars of a perfect pairing with coefficients in a field.

@[simp]

theorem LinearMap.restrictScalarsField_apply_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field K] [Field L] [Algebra K L] [AddCommGroup M] [AddCommGroup N] [Module L M] [Module L N] [Module K M] [Module K N] [IsScalarTower K L M] (p : M →ₗ[L] N →ₗ[L] L) {M' : Type u_5} {N' : Type u_6} [AddCommGroup M'] [AddCommGroup N'] [Module K M'] [Module K N'] [IsScalarTower K L N] (i : M' →ₗ[K] M) (j : N' →ₗ[K] N) (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range) (x : M') (y : N') : (algebraMap K L) (((i.restrictScalarsRange₂ j (Algebra.linearMap K L) ⋯ p hp) x) y) = (p (i x)) (j y)