English
Restricting scalars for a perfect pairing yields a new perfect pairing under suitable tower and restriction assumptions.
Русский
Ограничение скаляров для совершенного парирования даёт новое совершенное парирование при надлежащих условиях башни и ограничений.
LaTeX
$$PerfectPairing.restrictScalars (i,j) : PerfectPairing S M' N'$$
Lean4
/-- Restriction of scalars for a perfect pairing taking values in a subring. -/
@[deprecated IsPerfPair.restrictScalars (since := "2025-05-28")]
def _root_.PerfectPairing.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) : PerfectPairing S M' N' :=
{ toLinearMap :=
LinearMap.restrictScalarsRange₂ i j (Algebra.linearMap S R) (FaithfulSMul.algebraMap_injective S R) p hp
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)⟩ }
