toPretopology — Mathlib

Lean4
/-- The largest pretopology generating the given Grothendieck topology.

See [MM92] Chapter III, Section 2, Equations (3,4).
-/
def toPretopology (J : GrothendieckTopology C) : Pretopology C
    where
  coverings X := {R | Sieve.generate R ∈ J X}
  has_isos X Y f i := J.covering_of_eq_top (by simp)
  pullbacks X Y f R hR := by simpa [Sieve.pullbackArrows_comm] using J.pullback_stable f hR
  transitive X S Ti hS
    hTi := by
    apply J.transitive hS
    intro Y f
    rintro ⟨Z, g, f, hf, rfl⟩
    rw [Sieve.pullback_comp]
    apply J.pullback_stable g
    apply J.superset_covering _ (hTi _ hf)
    rintro Y g ⟨W, h, g, hg, rfl⟩
    exact ⟨_, h, _, ⟨_, _, _, hf, hg, rfl⟩, by simp⟩
Похожие утверждения