cofan_inj_naturality_symm — Mathlib

English

The naturality of injections with respect to a morphism Φ: S1 ⟶ S2 holds in a symmetric form with φ and injections on S1 and S2.

Русский

Натуральность инъекций относительно мoproта Φ: S1 ⟶ S2, выраженная в симметричной форме через φ и инъекции S1 и S2.

LaTeX

$$$(s.cofan(\Delta)).inj A \;\circ\; Φ.F.app Δ = Φ.f A.1.unop.len \;\circ\; (S2.s.cofan Δ).inj A$$$

Lean4

@[reassoc]
theorem cofan_inj_naturality_symm {S₁ S₂ : Split C} (Φ : S₁ ⟶ S₂) {Δ : SimplexCategoryᵒᵖ} (A : Splitting.IndexSet Δ) :
    (S₁.s.cofan Δ).inj A ≫ Φ.F.app Δ = Φ.f A.1.unop.len ≫ (S₂.s.cofan Δ).inj A := by
  rw [S₁.s.cofan_inj_eq, S₂.s.cofan_inj_eq, assoc, Φ.F.naturality, ← Φ.comm_assoc]

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