toPlus_plusLift — Mathlib

English

The natural transformation toPlus is compatible with plusLift, i.e., for any η: P → Q and a sheaf Q, the composition P → P⁺ → Q equals η; hence toPlus P; plusLift η hQ = η.

Русский

Совместимость toPlus с plusLift: композиция P → P⁺ → Q равна исходному η; то есть toPlus P; plusLift η hQ = η.

LaTeX

$$$ J.toPlus P \\; ; \\; J.plusLift η h_Q = η $$

Lean4

@[reassoc (attr := simp)]
theorem toPlus_plusLift {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) : J.toPlus P ≫ J.plusLift η hQ = η :=
  by
  dsimp [plusLift]
  rw [← Category.assoc]
  rw [Iso.comp_inv_eq]
  dsimp only [isoToPlus, asIso]
  rw [toPlus_naturality]

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