rTensor_injective_iff_lcomp_surjective

English

Injectivity of rTensor is equivalent to surjectivity of the left composition with f on character modules; this is a reformulation of the duality interplay.

Русский

Инъективность rTensor эквивалентна сюръективности левой композиции с f на характеристических модулях; отражает дуальную взаимосвязь.

LaTeX

$$$\text{Injective}(f) \iff \text{Surjective}(f \lrcorner\, \mathrm{CharacterModule})$$$

Lean4

theorem _root_.rTensor_injective_iff_lcomp_surjective {f : A →ₗ[R] A'} :
    Function.Injective (f.rTensor B) ↔ Function.Surjective (f.lcomp R <| CharacterModule B) := by
  simp [← dual_rTensor_conj_homEquiv, dual_surjective_iff_injective]

Похожие утверждения