map_inf_eq_map_inf_comap — Mathlib

English

An order isomorphism between submodule lattices is induced by a bijective semilinear map: toFun = map f, invFun = comap f.

Русский

Упорядоченный изоморфизм решетки подмодулов индуцирован биективным полуприводом: отображение = map f, обратное = comap f.

LaTeX

$$$\operatorname{orderIsoMapComapOfBijective} (f)\; (hf : Bijective\; f) : \operatorname{Submodule}\; R\; M \simeq_o \operatorname{Submodule}\; R_2\; M_2$$$

Lean4

theorem map_inf_eq_map_inf_comap [RingHomSurjective σ₁₂] {f : F} {p : Submodule R M} {p' : Submodule R₂ M₂} :
    map f p ⊓ p' = map f (p ⊓ comap f p') :=
  le_antisymm (by rintro _ ⟨⟨x, h₁, rfl⟩, h₂⟩; exact ⟨_, ⟨h₁, h₂⟩, rfl⟩)
    (le_inf (map_mono inf_le_left) (map_le_iff_le_comap.2 inf_le_right))

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