mapComp'_comp_whiskerLeft_mapComp'

English

Same as item 62937: In an adjunction L ⊣ R, if η_X is an isomorphism, then inv(L.map η_X) = ε_{L X}.

Русский

Так же, как и выше: при существовании единицы-изоморфизма η_X выполняется равенство инверсии.

LaTeX

$$$\\\\operatorname{inv}(L(\\\\eta_X)) = \\\\varepsilon_{L X}$$$

Lean4

@[reassoc]
theorem mapComp'_comp_whiskerLeft_mapComp' (hf : f₀₁ ≫ f₁₃ = f) :
    F.mapComp' f₀₁ f₁₃ f ≫ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃ =
      F.mapComp' f₀₂ f₂₃ f ≫ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫ (α_ _ _ _).hom :=
  by
  subst h₀₂ h₁₃ hf
  have := F.map₂_associator f₀₁ f₁₂ f₂₃
  simp only [Strict.associator_eqToIso, eqToIso.hom] at this
  simp [OplaxFunctor.mapComp', ← this, PrelaxFunctor.map₂_eqToHom]

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