cofan_inj_epi_naturality — Mathlib

English

For Δ1, Δ2 and A in IndexSet Δ1, with epi p, we have (s.cofan Δ1).inj A ≫ X.map p = (s.cofan Δ2).inj (A.epiComp p).

Русский

При Δ1, Δ2 и A ∈ IndexSet Δ1 и эпик-произведении p выполняется равенство: inj_A затем X.map p равняется inj_{A.epiComp p}.

LaTeX

$$$(s.cofan(\Delta_{1})).inj A \;\circ\; X.map p = (s.cofan(\Delta_{2})).inj (A.epiComp p)$$$

Lean4

@[reassoc]
theorem cofan_inj_epi_naturality {Δ₁ Δ₂ : SimplexCategoryᵒᵖ} (A : IndexSet Δ₁) (p : Δ₁ ⟶ Δ₂) [Epi p.unop] :
    (s.cofan Δ₁).inj A ≫ X.map p = (s.cofan Δ₂).inj (A.epiComp p) :=
  by
  dsimp [cofan]
  rw [assoc, ← X.map_comp]
  rfl

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