English
For an equivalence e: C ≃ D and sieve S on X, the double pushforward along e.functor and e.inverse equals the pullback along e.unitInv followed by e.inverse.
Русский
Для эквивалентности e: C ≃ D и щели S на X двойной перенос по e.functor и e.inverse равен pullback через e.unitInv затем применением e.inverse.
LaTeX
$$$S.functorPushforward e.functor = (S.pullback (e.unitInv.app X)).functorPullback e.inverse$$$
Lean4
/-- The Grothendieck topology associated to a topological space. -/
def grothendieckTopology : GrothendieckTopology (Opens T)
where
sieves X S := ∀ x ∈ X, ∃ (U : _) (f : U ⟶ X), S f ∧ x ∈ U
top_mem' _ _ hx := ⟨_, 𝟙 _, trivial, hx⟩
pullback_stable' X Y S f hf y
hy := by
rcases hf y (f.le hy) with ⟨U, g, hg, hU⟩
refine ⟨U ⊓ Y, homOfLE inf_le_right, ?_, hU, hy⟩
apply S.downward_closed hg (homOfLE inf_le_left)
transitive' X S hS R hR x
hx := by
rcases hS x hx with ⟨U, f, hf, hU⟩
rcases hR hf _ hU with ⟨V, g, hg, hV⟩
exact ⟨_, g ≫ f, hg, hV⟩
