toSheafify_sheafifyLift — Mathlib

English

The lift along a morphism and a sheaf is unique given the base equality condition.

Русский

Единственность подъема по морфизму и шефу при заданном условии равенства базы.

LaTeX

$$sheafifyLift_unique : ∀ η hQ γ, (toSheafify P ≫ γ = η) → γ = sheafifyLift J η hQ$$

Lean4

@[reassoc (attr := simp)]
theorem toSheafify_sheafifyLift {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) :
    J.toSheafify P ≫ sheafifyLift J η hQ = η :=
  by
  dsimp only [sheafifyLift, toSheafify]
  simp

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