cofan_inj_comp_app — Mathlib

English

For a morphism f: X ⟶ Y and a degree Δ with A ∈ IndexSet Δ, the composite of the cofan injection with f at Δ equals the φ-component with domain data, followed by Y-map.

Русский

Для морфизма f: X → Y и фиксированного Δ, A ∈ IndexSet Δ, композиция inj_A с f.app Δ равна компоненте φ f, соответствующей A, затем отображение Y.

LaTeX

$$$(s.cofan(\Delta).inj A) \;\circ\; f.app(\Delta) = \phi(f,A.1.unop.len) \;\circ\; Y.map(A.e.op)$$$

Lean4

@[reassoc (attr := simp)]
theorem cofan_inj_comp_app (f : X ⟶ Y) {Δ : SimplexCategoryᵒᵖ} (A : IndexSet Δ) :
    (s.cofan Δ).inj A ≫ f.app Δ = s.φ f A.1.unop.len ≫ Y.map A.e.op :=
  by
  simp only [cofan_inj_eq_assoc, φ, assoc]
  rw [NatTrans.naturality]

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