snd_δ — Mathlib

English

The derived pullback map δ interacts with φ₁ and τ₁ via g_desc.

Русский

Производный переход δ из горного соответствия взаимодействует с φ₁ и τ₁ через g_desc.

LaTeX

$$$\big(\mathrm{pullback.snd}(S.L_1.g, S.v_{01}.\\tau_3)\big) \circ S.\\delta = S.\\phi_1 \circ S.v_{23}.\\tau_1$$$

Lean4

@[reassoc (attr := simp)]
theorem snd_δ : (pullback.snd _ _ : S.P ⟶ _) ≫ S.δ = S.φ₁ ≫ S.v₂₃.τ₁ :=
  S.L₀'_exact.g_desc _ _

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