English
The interaction of the totalFlipIsoX with the first D-map D1 mirrors the compatibility with totalFlipIsoX_hom_D1: a commuting diagram with totalFlipIsoX and D1 holds.
Русский
Взаимодействие totalFlipIsoX с D1 удовлетворяет совместимости: диаграмма, сопряженная с totalFlipIsoX и D1, коммутирует.
LaTeX
$$$(K.totalFlipIsoX\ C\ j).hom \;\; \circ \; K.D_1\ c\ j\ j' = K.flip.D_2\ c\ j\ j' \; \circ \; (K.totalFlipIsoX\ c\ j').hom$$$
Lean4
@[reassoc]
theorem totalFlipIsoX_hom_D₂ (j j' : J) :
(K.totalFlipIsoX c j).hom ≫ K.D₂ c j j' = K.flip.D₁ c j j' ≫ (K.totalFlipIsoX c j').hom :=
by
by_cases h₀ : c.Rel j j'
· ext i₂ i₁ h₁
dsimp [totalFlipIsoX]
rw [ι_totalDesc_assoc, Linear.units_smul_comp, ι_D₂, ι_D₁_assoc]
dsimp
by_cases h₂ : c₂.Rel i₂ (c₂.next i₂)
· have h₃ : ComplexShape.π c₂ c₁ c (ComplexShape.next c₂ i₂, i₁) = j' := by
rw [← ComplexShape.next_π₁ c₁ c h₂ i₁, h₁, c.next_eq' h₀]
have h₄ : ComplexShape.π c₁ c₂ c (i₁, ComplexShape.next c₂ i₂) = j' := by rw [← h₃, ComplexShape.π_symm c₁ c₂ c]
rw [K.d₂_eq _ _ h₂ _ h₄, K.flip.d₁_eq _ h₂ _ _ h₃, Linear.units_smul_comp, assoc, ι_totalDesc,
Linear.comp_units_smul, smul_smul, smul_smul, ComplexShape.σ_ε₂ c₁ c i₁ h₂]
rfl
· rw [K.d₂_eq_zero _ _ _ _ h₂, K.flip.d₁_eq_zero _ _ _ _ h₂, smul_zero, zero_comp]
· rw [K.D₂_shape _ _ _ h₀, K.flip.D₁_shape c _ _ h₀, zero_comp, comp_zero]
