English
Restricting scalars of a perfect pairing to a subring preserves the perfect pairing structure under suitable injectivity and span conditions.
Русский
Ограничение скаляров совершенного парирования к подкольцу сохраняет структуру совершенного парирования при подходящих условиях инъективности и охвата.
LaTeX
$$PerfectPairing.restrictScalars (i,j) : PerfectPairing S M' N'$$
Lean4
/-- The restriction of a perfect pairing to submodules (expressed as injections to provide
definitional control). -/
@[deprecated IsPerfPair.restrict (since := "2025-05-28")]
def _root_.PerfectPairing.restrict : PerfectPairing R M' N'
where
toLinearMap := p.compl₁₂ i j
bijective_left := p.restrict_aux i j hi hj hij
bijective_right := p.flip.restrict_aux j i hj hi hij.flip
