English
Effective epis in a preregular category are stable under composition.
Русский
Эффективные эпимпии в прегеормрегулярной категории сохраняются при композиции.
LaTeX
$$instance instEffectiveEpiComp$$
Lean4
/-- Effective epis in a preregular category are stable under composition. -/
instance {Y Y' : C} (π : Y ⟶ X) [EffectiveEpi π] (π' : Y' ⟶ Y) [EffectiveEpi π'] : EffectiveEpi (π' ≫ π) :=
by
rw [effectiveEpi_iff_effectiveEpiFamily, ← Sieve.effectiveEpimorphic_family]
suffices h₂ : (Sieve.generate (Presieve.ofArrows _ _)) ∈ (regularTopology C) X
by
change Nonempty _
rw [← Sieve.forallYonedaIsSheaf_iff_colimit]
exact fun W => regularTopology.isSheaf_yoneda_obj W _ h₂
apply Coverage.Saturate.transitive X (Sieve.generate (Presieve.ofArrows (fun () ↦ Y) (fun () ↦ π)))
· apply Coverage.Saturate.of
use Y, π
· intro V f ⟨Y₁, h, g, ⟨hY, hf⟩⟩
rw [← hf, Sieve.pullback_comp]
apply (regularTopology C).pullback_stable'
apply regularTopology.mem_sieves_of_hasEffectiveEpi
cases hY
exact ⟨Y', π', inferInstance, Y', (𝟙 _), π' ≫ π, Presieve.ofArrows.mk (), (by simp)⟩
