pullback_comp — Mathlib

English

For any arrows g: Z → Y and f: Y → X and any sieve S on X, pulling back along the composition g ∘ f is the same as pulling back along f and then along g.

Русский

Пусть g: Z → Y и f: Y → X и дано сито S на X. Обратное по композиции g ∘ f равно последовательному обратному по f, затем по g.

LaTeX

$$$ S.pullback (g \\circ f) = (S.pullback f).pullback g $$$

Lean4

theorem pullback_comp {f : Y ⟶ X} {g : Z ⟶ Y} (S : Sieve X) : S.pullback (g ≫ f) = (S.pullback f).pullback g := by
  simp [Sieve.ext_iff]

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