regularCoverage — Mathlib

Lean4
/-- The regular coverage on a regular category `C`.
-/
def regularCoverage [Preregular C] : Coverage C
    where
  coverings
    B := {S | ∃ (X : C) (f : X ⟶ B), S = Presieve.ofArrows (fun (_ : Unit) ↦ X) (fun (_ : Unit) ↦ f) ∧ EffectiveEpi f}
  pullback := by
    intro X Y f S ⟨Z, π, hπ, h_epi⟩
    have := Preregular.exists_fac f π
    obtain ⟨W, h, _, i, this⟩ := this
    refine ⟨Presieve.singleton h, ⟨?_, ?_⟩⟩
    ·
      exact
        ⟨W, h, by { rw [Presieve.ofArrows_pUnit h]
        }, inferInstance⟩
    · intro W g hg
      cases hg
      refine ⟨Z, i, π, ⟨?_, this⟩⟩
      cases hπ
      rw [Presieve.ofArrows_pUnit]
      exact Presieve.singleton.mk
Похожие утверждения