instRightRigidCategory — Mathlib

English

If V is right rigid, then Action V H is right rigid; the right rigidity transfers along the equivalence.

Русский

Если V правосторонне жесткая, то Action V H жесткая справа; жесткость сохраняется через эквиваленцию.

LaTeX

$$$\text{RightRigidCategory}(\mathrm{Action}(V,H))$$$

Lean4

/-- If `V` is right rigid, so is `Action V G`. -/
instance [RightRigidCategory V] : RightRigidCategory (Action V H) :=
  rightRigidCategoryOfEquivalence (functorCategoryEquivalence V H).toAdjunction

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