hasLeftCalculusOfFractions' — Mathlib

English

If adjunction F ⊣ G holds with F full and faithful, then the right category of fractions relative to W admits a left calculus of fractions under the inverse-image of isomorphisms.

Русский

Если существует адъюнкция F ⊣ G с полной и верной F, тогда левая дробная система существует для соответствующей инвертируемой подкатегории.

LaTeX

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

Lean4

theorem hasLeftCalculusOfFractions' (adj : G ⊣ F) : ((isomorphisms C₂).inverseImage G).HasLeftCalculusOfFractions :=
  hasLeftCalculusOfFractions adj _ (fun _ _ _ h ↦ h) adj.functorCategory_inverseImage_isomorphisms_unit

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