surjectivity — Mathlib

English

The surjectivity functor f is an isomorphism in the presentable setting for z in c.pt.

Русский

Для z в c.pt отображение f является изоморфизмом в презентируемой обстановке.

LaTeX

$$$\text{IsIso } (\text{surjectivity}.f z)$$$

Lean4

theorem surjectivity [∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
    [IsCardinalFiltered J κ] (hXκ : HasCardinalLT (Subobject X) κ) (z : X ⟶ c.pt) :
    ∃ (j₀ : J) (y : X ⟶ Y.obj j₀), z = y ≫ c.ι.app j₀ :=
  by
  have := isFiltered_of_isCardinalFiltered J κ
  have := hc.mono_ι_app_of_isFiltered
  have := NatTrans.mono_of_mono_app c.ι
  obtain ⟨j, _⟩ := exists_isIso_of_functor_from_monoOver (F z) hXκ _ (colimit.isColimit _) (f z) (hf z) (epi_f hc z)
  refine ⟨j, inv ((F z).obj j).obj.hom ≫ (pullback.fst c.ι _).app j, ?_⟩
  dsimp
  rw [Category.assoc, IsIso.eq_inv_comp, ← NatTrans.comp_app, pullback.condition, NatTrans.comp_app,
    Functor.const_map_app]

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