functorFullOfMono — Mathlib

English

If f is open and mono, the induced functor on opens is full.

Русский

Если f является открытым моно-отображением, индуцированный функтор на множестве открытых множеств полон.

LaTeX

$$$ \text{If } hf \text{ is open and mono, then } hf.functor \text{ is full.}$$$

Lean4

instance functorFullOfMono {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap f) [H : Mono f] : hf.functor.Full where
  map_surjective
    i :=
    ⟨homOfLE fun x hx => by
        obtain ⟨y, hy, eq⟩ := i.le ⟨x, hx, rfl⟩
        exact (TopCat.mono_iff_injective f).mp H eq ▸ hy,
      rfl⟩

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