English
A scalar restriction construction yields a new perfect pairing from the existing one, provided the scalar maps satisfy compatibility and injectivity assumptions.
Русский
Ограничение скаляров порождает новое совершенное парирование из существующего, при условии совместимости отображений и инъективности.
LaTeX
$$PerfectPairing.restrictScalars : PerfectPairing S M' N'$$
Lean4
/-- Restricting a perfect pairing to a subring of the scalars results in a perfect pairing. -/
theorem restrictScalars (hi : Injective i) (hj : Injective j) (hM : span R (LinearMap.range i : Set M) = ⊤)
(hN : span R (LinearMap.range j : Set N) = ⊤)
(h₁ : ∀ g : Module.Dual S N', ∃ m, (p.toPerfPair (i m)).restrictScalars S ∘ₗ j = Algebra.linearMap S R ∘ₗ g)
(h₂ : ∀ g : Module.Dual S M', ∃ n, (p.flip.toPerfPair (j n)).restrictScalars S ∘ₗ i = Algebra.linearMap S R ∘ₗ g)
(hp : ∀ m n, p (i m) (j n) ∈ (algebraMap S R).range) :
(LinearMap.restrictScalarsRange₂ i j (Algebra.linearMap S R) (FaithfulSMul.algebraMap_injective S R) p
hp).IsPerfPair
where
bijective_left := ⟨p.restrictScalars_injective_aux i j hi hN hp, p.restrictScalars_surjective_aux i j h₁ hp⟩
bijective_right :=
⟨p.flip.restrictScalars_injective_aux j i hj hM fun m n ↦ hp n m,
p.flip.restrictScalars_surjective_aux j i h₂ fun m n ↦ hp n m⟩
