English
For an equivalence e, the right zigzag hom equals the composition of ρ_inv and λ_inv.
Русский
Для эквивалентности e правая зигзагообразная гом равна композиции ρ_inv и λ_inv.
LaTeX
$$$\\mathrm{right\_triangle\_hom}(e) : \\; \\mathrm{rightZigzag\_hom} = (\\rho_{e.inv}).hom \\; ⋅ \\; (\\lambda_{e.inv}).inv$$$
Lean4
/-- Suppose we have a square of 1-morphisms (where the top and bottom are adjunctions `l₁ ⊣ r₁`
and `l₂ ⊣ r₂` respectively).
```
c ↔ d
g ↓ ↓ h
e ↔ f
```
Then we have a bijection between natural transformations `g ≫ l₂ ⟶ l₁ ≫ h` and
`r₁ ≫ g ⟶ h ≫ r₂`. This can be seen as a bijection of the 2-cells:
```
l₁ r₁
c --→ d c ←-- d
g ↓ ↗ ↓ h g ↓ ↘ ↓ h
e --→ f e ←-- f
L₂ R₂
```
Note that if one of the transformations is an iso, it does not imply the other is an iso.
-/
@[simps! -isSimp]
def mateEquiv : (g ≫ l₂ ⟶ l₁ ≫ h) ≃ (r₁ ≫ g ⟶ h ≫ r₂) :=
adj₂.homEquiv₂.trans ((Iso.homCongr (Iso.refl _) (α_ _ _ _)).trans adj₁.homEquiv₁)
