inhabitedGradedObject — Mathlib

English

The inverse of the right unitor at j equals the composition of e.inv and the map of the inverse of singleObjApplyIso, followed by ιMapBifunctorMapObj.

Русский

Обратный к правому унитору на j равен композиции e.inv, отображения обратного к singleObjApplyIso и затем ιMapBifunctorMapObj.

LaTeX

$$$ (mapBifunctorRightUnitor F Y e p hp X).inv j = e.inv.app (X j) \\\\; \\\\; ≫ \\\\; (F.map (singleObjApplyIso (0 : I) Y).inv).app (X j) \\\\; \\\\; ιMapBifunctorMapObj F p X ((single₀ I).obj Y) j 0 j (hp j) $$$

Lean4

instance inhabitedGradedObject (β : Type w) (C : Type u) [Inhabited C] : Inhabited (GradedObject β C) :=
  ⟨fun _ => Inhabited.default⟩
    -- `s` is here to distinguish type synonyms asking for different shifts

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