giMapComap — Mathlib

English

If f is surjective, the pair (map f, comap f) forms a Galois insertion between submodules, linking images and preimages.

Русский

Если f сюръективно, пара (map f, comap f) образует вложение Гало между подмодулями, устанавливая связь между образами и предобразами.

LaTeX

$$GaloisInsertion (map f) (comap f)$$

Lean4

/-- `map f` and `comap f` form a `GaloisInsertion` when `f` is surjective. -/
def giMapComap (hf : Surjective f) : GaloisInsertion (map f) (comap f) :=
  (gc_map_comap f).toGaloisInsertion fun S x hx =>
    by
    rcases hf x with ⟨y, rfl⟩
    simp only [mem_map, mem_comap]
    exact ⟨y, hx, rfl⟩

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