XXIsoOfEq_hom_ιTotal — Mathlib

English

A specialized equality of the XXIsoOfEq hom component with a total inclusion when indices are equal.

Русский

Специализированное равенство гом-компоненты XXIsoOfEq с инклюзией total при равенстве индексов.

LaTeX

$$$\\text{(XXIsoOfEq} \\; K \\; c_{12} \\; h_1 \\; h_2).hom \\; \\circ \\; ιTotal c_{12} y_1 y_2 i_{12} h = ιTotal c_{12} x_1 x_2 i_{12} (by rw [h_1, h_2, h])$$$

Lean4

@[reassoc (attr := simp)]
theorem XXIsoOfEq_hom_ιTotal {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ : x₂ = y₂) (i₁₂ : I₁₂)
    (h : ComplexShape.π c₁ c₂ c₁₂ (y₁, y₂) = i₁₂) :
    (K.XXIsoOfEq _ _ _ h₁ h₂).hom ≫ K.ιTotal c₁₂ y₁ y₂ i₁₂ h = K.ιTotal c₁₂ x₁ x₂ i₁₂ (by rw [h₁, h₂, h]) :=
  by
  subst h₁ h₂
  simp

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