snd_δ_inr — Mathlib

English

A pushout/pullback compatibility expresses δ in terms of φ₁ and φ₂ with inr and inl maps.

Русский

Совместимости дельты в рамках пушпута/пуллбэка выражают δ через φ₁ и φ₂ с inr и inl.

LaTeX

$$$(pullback.snd(S.L_1.g, S.v_{01}.\\tau_3)) \\circ S.\\delta \\circ (\\mathrm{pushout.inr}(S.L_2.f, S.v_2 3.\\tau_1)) = (\\mathrm{pullback.fst}(S.L_1.g, S.v_{01}.\\tau_3)) \\circ S.v_{12}.\\tau_2 \\circ (\\mathrm{pushout.inl}(S.L_2.f, S.v_{23}.\\tau_1))$$$

Lean4

theorem snd_δ_inr :
    (pullback.snd _ _ : S.P ⟶ _) ≫ S.δ ≫ (pushout.inr _ _ : _ ⟶ S.P') = pullback.fst _ _ ≫ S.v₁₂.τ₂ ≫ pushout.inl _ _ :=
  by simp only [snd_δ_assoc, ← pushout.condition, φ₂, φ₁_L₂_f_assoc, assoc]

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