English
Two morphisms are equal if they agree on all π-slices due to the extensional principle for the map produced by mapBifunctor.
Русский
Два морфизма равны, если они согласованы на всех π-срезах, следуя экстенту для отображения mapBifunctor.
LaTeX
$$$f = g \\;\\text{iff} \\; f|_{\\text{slice}(i_1,i_2,i_3)} = g|_{\\text{slice}(i_1,i_2,i_3)} \\;\\forall i_1,i_2,i_3$$$
Lean4
@[reassoc (attr := simp)]
theorem ι_D₃ :
ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' = d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j' :=
by
simp only [ι_eq _ _ _ _ _ _ _ _ _ _ _ _ rfl h, D₃, assoc, mapBifunctor.ι_D₂]
by_cases h₁ : c₃.Rel i₃ (c₃.next i₃)
· rw [d₃_eq _ _ _ _ _ _ _ _ _ h₁]
by_cases h₂ : ComplexShape.π c₁₂ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), c₃.next i₃) = j'
·
rw [mapBifunctor.d₂_eq _ _ _ _ _ h₁ _ h₂, ιOrZero_eq _ _ _ _ _ _ _ _ _ _ _ h₂, Linear.comp_units_smul,
smul_left_cancel_iff, ι_eq _ _ _ _ _ _ _ _ _ _ _ _ rfl h₂, NatTrans.naturality_assoc]
·
rw [mapBifunctor.d₂_eq_zero' _ _ _ _ _ h₁ _ h₂, comp_zero, ιOrZero_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₂, comp_zero,
smul_zero]
· rw [mapBifunctor.d₂_eq_zero _ _ _ _ _ _ _ h₁, comp_zero, d₃_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₁]
