pullback — Mathlib

English

Pullback formulation showing how mk aligns with pullback across a morphism f.

Русский

Формулировка pullback, показывающая соответствие mk через вытяжку по морфизму f.

LaTeX

$$$\text{pullback}(mk x) = mk (x.Pullback f)$$$

Lean4

/-- Pull back a term of `Meq P S` with respect to a morphism `f : Y ⟶ X` in `C`. -/
def pullback {Y X : C} {P : Cᵒᵖ ⥤ D} {S : J.Cover X} (x : Meq P S) (f : Y ⟶ X) : Meq P ((J.pullback f).obj S) :=
  ⟨fun I => x ⟨_, I.f ≫ f, I.hf⟩, fun I => x.condition (GrothendieckTopology.Cover.Relation.mk' I.r.base)⟩

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