whiskerLeft_mapId_inv — Mathlib

English

If α: r1 → r2 has a conjugate (via conjugateEquiv adj1 adj2).symm that is an isomorphism, then α is an isomorphism.

Русский

Если α: r1 → r2 имеет коньюгат через симм и он является изоморфизмом, то α изоморфизм.

LaTeX

$$$\\forall \\alpha:\\ r_1\\to r_2,\\ IsIso\\big((\\mathrm{conjugateEquiv}\\ adj_1\\ adj_2).symm\\alpha\\big) \\Rightarrow IsIso(\\alpha)$$$

Lean4

@[reassoc, to_app]
theorem whiskerLeft_mapId_inv (f : a ⟶ b) :
    F.map f ◁ (F.mapId b).inv = (ρ_ (F.map f)).hom ≫ F.map₂ (ρ_ f).inv ≫ (F.mapComp f (𝟙 b)).hom := by
  simpa using congrArg (·.inv) (F.whiskerLeftIso_mapId f)

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