app_cond — Mathlib

English

For forgetful functors from A' to Type with limit-preserving properties, IsSheaf J P' is equivalent to IsSheaf J (P' ⋙ s).

Русский

Для забывающих функторов из A' в Type, сохраняющих пределы, IsSheaf J P' эквивалентно IsSheaf J (P' ⋙ s).

LaTeX

$$$IsSheaf(J, P') \iff IsSheaf(J, P'\circ s)$$$

Lean4

theorem app_cond (hx : x.Compatible) (g : Y ⟶ X) {Z : C} (p : Z ⟶ Y) (hp : S (p ≫ g)) :
    app hG x hx g ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app ⟨Over.mk (𝟙 Z)⟩ :=
  (exists_app hG x hx g).choose_spec p hp

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