invtSubmodule — Mathlib

English

The infimum of two f-invariant submodules is f-invariant.

Русский

Нижняя граница двух подмодулей, инвариантных по f, также инвариантна по f.

LaTeX

$$inf_mem: p ∈ f.invtSubmodule ∧ q ∈ f.invtSubmodule → p ⊓ q ∈ f.invtSubmodule$$

Lean4

/-- Given an endomorphism, `f` of some module, this is the sublattice of all `f`-invariant
submodules. -/
def invtSubmodule : Sublattice (Submodule R M)
    where
  carrier := {p : Submodule R M | p ≤ p.comap f}
  supClosed' p hp q
    hq :=
    sup_le_iff.mpr ⟨le_trans hp <| Submodule.comap_mono le_sup_left, le_trans hq <| Submodule.comap_mono le_sup_right⟩
  infClosed' p hp q
    hq := by
    simp only [Set.mem_setOf_eq, Submodule.comap_inf, le_inf_iff]
    exact ⟨inf_le_of_left_le hp, inf_le_of_right_le hq⟩

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