fullyInvariantSubmodule — Mathlib

English

For an ideal I, the statement that I is fully invariant is equivalent to I being two-sided.

Русский

Для идеала I утверждение о полной инвариантности эквивалентно тому, что I двусторонний.

LaTeX

$$$$ I \\text{ IsFullyInvariant } \\iff I \\text{ IsTwoSided}. $$$$

Lean4

/-- The fully invariant submodules of a module form a complete sublattice in the lattice of
submodules. -/
def fullyInvariantSubmodule : CompleteSublattice (Submodule R M) :=
  .mk' {N : Submodule R M | N.IsFullyInvariant}
    (fun _s hs f ↦ sSup_le fun _N hN ↦ (hs hN f).trans <| Submodule.comap_mono <| le_sSup hN) fun _s hs f ↦
    Submodule.map_le_iff_le_comap.mp <|
      le_sInf fun _N hN ↦ Submodule.map_le_iff_le_comap.mpr <| (sInf_le hN).trans (hs hN f)

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