giMapComap — Mathlib

English

If f is surjective, then map f is surjective as a function on ideals.

Русский

Если f сюръективна, то map f является сюръективной функцией на идеалах.

LaTeX

$$$\\text{Surjective}(\\operatorname{map} f)$ given $\\text{Surjective}(f)$$$

Lean4

/-- `map` and `comap` are adjoint, and the composition `map f ∘ comap f` is the
  identity -/
def giMapComap : GaloisInsertion (map f) (comap f) :=
  GaloisInsertion.monotoneIntro (gc_map_comap f).monotone_u (gc_map_comap f).monotone_l (fun _ => le_comap_map)
    (map_comap_of_surjective _ hf)

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