plusMap_plusLift — Mathlib

English

For P, Q, R and arrows η: P → Q, γ: Q → R with R a sheaf, the composite of plusMap with plusLift equals the plusLift of the composite, i.e., plusMap η followed by plusLift γ equals plusLift of η ∘ γ.

Русский

Для P, Q, R и стрел η: P → Q, γ: Q → R, где R — шейф, композиция plusMap η затем plusLift γ равна plusLift (η ∘ γ).

LaTeX

$$$ J.plusMap \\eta \\; \\circ \\; J.plusLift \\gamma h_R = J.plusLift (\\eta \\circ γ) h_R $$$

Lean4

@[simp]
theorem plusMap_plusLift {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : Presheaf.IsSheaf J R) :
    J.plusMap η ≫ J.plusLift γ hR = J.plusLift (η ≫ γ) hR :=
  by
  apply J.plusLift_unique
  rw [← Category.assoc, ← J.toPlus_naturality, Category.assoc, J.toPlus_plusLift]

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