map₁_yonedaEquivFst — Mathlib

English

map₁ is compatible with composition: map₁(η ≫ μ) = map₁(μ) ∘ map₁(η).

Русский

map₁ совместим с композициями: map₁(η ≫ μ) = map₁(μ) ∘ map₁(η).

LaTeX

$$$\\forall {\\eta : F ⟶ G} {\\mu : G ⟶ H},\\; YonedaCollection.map₁ (\\eta ≫ μ) (X := X) =\\; ( YonedaCollection.map₁ μ (X := X)) \\circ ( YonedaCollection.map₁ \\eta (X := X))$$$

Lean4

@[simp]
theorem map₁_yonedaEquivFst {G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (η : F ⟶ G) (p : YonedaCollection F X) :
    (YonedaCollection.map₁ η p).yonedaEquivFst = p.yonedaEquivFst := by
  simp only [YonedaCollection.yonedaEquivFst_eq, map₁_fst]

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