injective_characterModule_iff_rTensor_preserves_injective_linearMap

English

The injectivity of the character module functor is equivalent to the rTensor functor being injective for every f.

Русский

Инъективность характеристического модуля эквивалентна инъективности rTensor-функтора для каждого f.

LaTeX

$$$\\text{Injective}(\\mathrm{CharacterModule}(M)) \\iff \\forall f, \\mathrm{Injective}(f.rTensor M)$$$

Lean4

/-- Define the character module of `M` to be `M →+ ℚ ⧸ ℤ`.
The character module of `M` is an injective module if and only if
`f ⊗ 𝟙 M` is injective for any linear map `f` in the same universe as `M`.
-/
theorem injective_characterModule_iff_rTensor_preserves_injective_linearMap :
    Module.Injective R (CharacterModule M) ↔
      ∀ ⦃N N' : Type v⦄ [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N'] (f : N →ₗ[R] N'),
        Function.Injective f → Function.Injective (f.rTensor M) :=
  by simp_rw [injective_iff, rTensor_injective_iff_lcomp_surjective, Surjective, DFunLike.ext_iff]; rfl

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