over — Mathlib

Lean4
/-- The Grothendieck topology on the category `Over X` for any `X : C` that is
induced by a Grothendieck topology on `C`. -/
def over (X : C) : GrothendieckTopology (Over X)
    where
  sieves Y S := Sieve.overEquiv Y S ∈ J Y.left
  top_mem'
    Y := by
    change _ ∈ J Y.left
    simp
  pullback_stable' Y₁ Y₂ S₁ f
    h₁ := by
    change _ ∈ J _ at h₁ ⊢
    rw [Sieve.overEquiv_pullback]
    exact J.pullback_stable _ h₁
  transitive' Y S (hS : _ ∈ J _) R
    hR :=
    J.transitive hS _
      (fun Z f hf => by
        have hf' : _ ∈ J _ := hR ((Sieve.overEquiv_iff _ _).1 hf)
        rw [Sieve.overEquiv_pullback] at hf'
        exact hf')
Похожие утверждения