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.

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 : PerfectPairing R M N) {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

• p.restrict i j hi hj hij = { toLin := p.toLin.compl₁₂ i j, bijectiveLeft := ⋯, bijectiveRight := ⋯ }

@[simp]

theorem PerfectPairing.restrict_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] (p : PerfectPairing R M N) {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)) : (p.restrict i j hi hj hij).toLin = p.toLin.compl₁₂ i j

@[simp]

theorem PerfectPairing.restrict_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) {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)) (x : M') (y : N') : ((p.restrict i j hi hj hij) x) y = (p (i x)) (j y)

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 : PerfectPairing R M N) {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.toDualLeft (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g) (h₂ : ∀ (g : Module.Dual S M'), ∃ (n : N'), ↑S (p.toDualRight (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

• p.restrictScalars i j hi hj hM hN h₁ h₂ hp = { toLin := PerfectPairing.restrictScalarsAux✝ p i j hp, bijectiveLeft := ⋯, bijectiveRight := ⋯ }

theorem PerfectPairing.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 : PerfectPairing L M N) (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 : Basis (Fin n) L M) (b' : 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][bourbaki1989].

def PerfectPairing.restrictScalarsField {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 : PerfectPairing L M N) {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 ↑(LinearMap.range i)) (Submodule.span L ↑(LinearMap.range j))) (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range) : PerfectPairing K M' N'

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

Equations

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

@[simp]

theorem PerfectPairing.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 : PerfectPairing L M N) {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 ↑(LinearMap.range i)) (Submodule.span L ↑(LinearMap.range j))) (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range) (x : M') (y : N') : (algebraMap K L) (((p.restrictScalarsField i j hi hj hij hp) x) y) = (p (i x)) (j y)