arrowHomEquiv_apply_right_fst — Mathlib

English

In this pullback situation, π followed by fst equals the map induced by G.map f1.op at X3.

Русский

В данной ситуации вытягивания, композиция π затем fst равна отображению, задаваемому через G.map f1.op на X3.

LaTeX

$$$π \\;\\; ∘ \\; fst = (G.map f_1.op).app X_3$$$

Lean4

@[reassoc (attr := simp)]
theorem arrowHomEquiv_apply_right_fst (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) :
    ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α).right ≫ sq₁₃.fst = adj₂.homEquiv (sq₁₂.inr ≫ α.left) :=
  IsPullback.lift_fst _ _ _ _

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