instPreregularOfPrecoherentOfHasFiniteCoproducts

English

If a sieve contains a finite EffectiveEpiFamily indexed by Y π, then it belongs to the coherent topology.

Русский

Если сито содержит конечную EffectiveEpiFamily, индексированную Y π, то оно принадлежит когерентной топологии.

LaTeX

$$CategoryTheory.coherentTopology.mem_sieves_of_hasEffectiveEpiFamily$$

Lean4

instance [Precoherent C] [HasFiniteCoproducts C] : Preregular C where
  exists_fac {X Y Z} f g
    _ := by
    have hp := Precoherent.pullback f PUnit (fun () ↦ Z) (fun () ↦ g)
    simp only [exists_const] at hp
    rw [← effectiveEpi_iff_effectiveEpiFamily g] at hp
    obtain ⟨β, _, X₂, π₂, h, ι, hι⟩ := hp inferInstance
    refine ⟨∐ X₂, Sigma.desc π₂, inferInstance, Sigma.desc ι, ?_⟩
    ext b
    simpa using hι b

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