unitForward_naturality₁ — Mathlib

English

In naturality one, for ε: F → G with hε: ε ≫ μ = η, and X, p in YonedaCollection (restrictedYonedaObj η) X, we have: unitForward μ X (p.map₁ (restrictedYonedaObjMap₁ ε hε)) = ε.app _ (unitForward η X p).

Русский

В натуральности 1 для ε: F → G с hε: ε ≫ μ = η, и для X, p ∈ YonedaCollection (restrictedYonedaObj η) X выполняется: unitForward μ X (p.map₁ (restrictedYonedaObjMap₁ ε hε)) = ε.app _ (unitForward η X p).

LaTeX

$$$$ unitForward\ \mu\ X\ (p\map_1 (restrictedYonedaObjMap_1\ \varepsilon\ h\varepsilon)) = \varepsilon.app\ _\ (unitForward\ \eta\ X\ p) $$$$

Lean4

@[simp]
theorem unitForward_naturality₁ {F G : Cᵒᵖ ⥤ Type v} {η : F ⟶ A} {μ : G ⟶ A} (ε : F ⟶ G) (hε : ε ≫ μ = η) (X : C)
    (p : YonedaCollection (restrictedYonedaObj η) X) :
    unitForward μ X (p.map₁ (restrictedYonedaObjMap₁ ε hε)) = ε.app _ (unitForward η X p) := by simp [unitForward]

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