bindToBase — Mathlib

English

There exists a canonical morphism from the glued sieve S.bind T to the base sieve S in a Grothendieck topology setting; this map is defined by downward-closedness using the given data.

Русский

Существует каноническое морфизм S.bind T → S в рамках топологии Гротендика; отображение задаётся через нисходящее замыкание и данные на S.

LaTeX

$$$\\text{bindToBase}(S,T) : S.bind T \\to S$$$

Lean4

/-- The canonical morphism from `S.bind T` to `T`. -/
def bindToBase {X : C} (S : J.Cover X) (T : ∀ I : S.Arrow, J.Cover I.Y) : S.bind T ⟶ S :=
  homOfLE <| by
    rintro Y f ⟨Z, e1, e2, h1, _, h3⟩
    rw [← h3]
    apply Sieve.downward_closed
    exact h1

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