hasRightCalculusOfFractions — Mathlib

English

Dually, the right calculus of fractions holds for adjunctions with W, via opposite categories.

Русский

Двойственно, правое исчисление дробей справедливо для сопряжений с W через противоположные категории.

LaTeX

$$$\\text{hasRightCalculusOfFractions}(adj,W)$$$

Lean4

theorem hasRightCalculusOfFractions (adj : F ⊣ G) (W : MorphismProperty C₁) [W.IsMultiplicative] (hW : W.IsInvertedBy G)
    (hW' : (W.functorCategory _) adj.counit) : W.HasRightCalculusOfFractions :=
  have := hasLeftCalculusOfFractions adj.op W.op hW.op (fun _ ↦ hW' _)
  inferInstanceAs W.op.unop.HasRightCalculusOfFractions

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