isInternal_submodule_of_iSupIndep_of_iSup_eq_top

English

Given iSupIndep A and iSup A = ⊤, A is internal.

Русский

При iSupIndep(A) и iSup(A) = ⊤ подмодули образуют внутреннее разложение.

LaTeX

$$isInternal_submodule_of_iSupIndep_of_iSup_eq_top {A} (hi) (hs) : IsInternal A$$

Lean4

/-- Note that this is not generally true for `[Semiring R]`; see
`iSupIndep.dfinsupp_lsum_injective` for details. -/
theorem isInternal_submodule_of_iSupIndep_of_iSup_eq_top {A : ι → Submodule R M} (hi : iSupIndep A) (hs : iSup A = ⊤) :
    IsInternal A :=
  ⟨hi.dfinsupp_lsum_injective,
    -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specify value of `f`
    (LinearMap.range_eq_top (f := DFinsupp.lsum _ _)).1 <| (Submodule.iSup_eq_range_dfinsupp_lsum _).symm.trans hs⟩

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