English
With η and ε satisfying the left triangle condition, the right zigzag is idempotent: rightZigzag η ε ⊗≫ rightZigzag η ε = rightZigzag η ε.
Русский
При η и ε, удовлетворяющих левому треугольнику, правый зигзаг идемпотентен: право-зигзаг η ε ⊗≫ право-зигзаг η ε = право-зигзаг η ε.
LaTeX
$$$$ \text{rightZigzag } \eta \epsilon \; \otimes\!\gg \; \text{rightZigzag } \eta \epsilon = \text{rightZigzag } \eta \epsilon, $$$$
Lean4
theorem rightZigzag_idempotent_of_left_triangle (η : 𝟙 a ⟶ f ≫ g) (ε : g ≫ f ⟶ 𝟙 b)
(h : leftZigzag η ε = (λ_ _).hom ≫ (ρ_ _).inv) : rightZigzag η ε ⊗≫ rightZigzag η ε = rightZigzag η ε :=
by
dsimp only [rightZigzag]
calc
_ = g ◁ η ⊗≫ ((ε ▷ g ▷ 𝟙 a) ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g := by bicategory
_ = 𝟙 _ ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 _ := by rw [← whisker_exchange];
bicategory
_ = g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g := by rw [← whisker_exchange, ← whisker_exchange, leftZigzag];
bicategory
_ = g ◁ η ⊗≫ ε ▷ g := by rw [h]; bicategory
