hasRightCalculusOfFractions' — Mathlib

English

The inverse-image of isomorphisms along G yields a right calculus of fractions in the associated localized setting.

Русский

Обратное изображение изоморфизмов вдоль G обеспечивает правый расчёт дробей в локализованной структуре.

LaTeX

$$$((\mathrm{isomorphisms}(C_2)).inverseImage G).\text{HasRightCalculusOfFractions}$$$

Lean4

theorem hasRightCalculusOfFractions' (adj : F ⊣ G) : ((isomorphisms C₂).inverseImage G).HasRightCalculusOfFractions :=
  hasRightCalculusOfFractions adj _ (fun _ _ _ h ↦ h) adj.functorCategory_inverseImage_isomorphisms_counit

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