δ_eq — Mathlib

English

In SnakeInput, given compatible morphisms x₃, x₂, x₁ and relations h₂, h₁, the δ-map commutes with the outer composites: x₃ ≫ δ = x₁ ≫ v₂₃.τ₁.

Русский

В SnakeInput, при совместимых морфизмах и равенствах, δ-компонентная карта компонуется слева и справа так: x₃ ≫ δ = x₁ ≫ v₂₃.τ₁.

LaTeX

$$$ x_3 \circ S.δ = x_1 \circ S.v_{2 3}.τ_1 $$$

Lean4

theorem δ_eq {A : C} (x₃ : A ⟶ S.L₀.X₃) (x₂ : A ⟶ S.L₁.X₂) (x₁ : A ⟶ S.L₂.X₁) (h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃)
    (h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂) : x₃ ≫ S.δ = x₁ ≫ S.v₂₃.τ₁ :=
  by
  have H := (pullback.lift x₂ x₃ h₂) ≫= S.snd_δ
  rw [pullback.lift_snd_assoc] at H
  rw [H, ← assoc]
  congr 1
  simp only [← cancel_mono S.L₂.f, assoc, φ₁_L₂_f, lift_φ₂, h₁]

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