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 i.range j.range)
:
(p.compl₁₂ i j).IsPerfPair
The restriction of a perfect pairing to submodules is a perfect pairing.
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 ↑i.range = ⊤)
(hN : Submodule.span R ↑j.range = ⊤)
(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.
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.finrank_eq_of_isPerfPair
{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)
:
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 ↑i.range) (Submodule.span L ↑j.range))
(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)