sheafifyMap_comp — Mathlib

English

A repeat formulation of toSheafify_naturality expresses the same commutativity for the specific morphism between presheaves in the adjunction context.

Русский

Повторная формулировка естественности toSheafify_naturality для конкретного морфизма между прешейфами в контексте адъюнкции.

LaTeX

$$$\text{toSheafify}_\text{naturality} : \; \eta \circ toSheafify = toSheafify \circ sheafifyMap(\eta).$$$

Lean4

@[simp]
theorem sheafifyMap_comp {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) :
    sheafifyMap J (η ≫ γ) = sheafifyMap J η ≫ sheafifyMap J γ := by simp [sheafifyMap, sheafify]

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