op — Mathlib · SciLib

English

If W has a right calculus of fractions, then its opposite W.op has a left calculus of fractions, with explicit existence of left fractions transported via op.

Русский

Если W обладает правой теорией дробей, то ее противоположная W.op имеет левую теорию дробей, существование левых дробей переносится через операцию Opposite.

LaTeX

$$$\forall {C} [\text{Category } C], W : MorphismProperty C, [W.HasRightCalculusOfFractions] \Rightarrow W.op.HasLeftCalculusOfFractions$$$

Lean4

/-- The left fraction in the opposite category corresponding to a right fraction. -/
@[simps]
def op {X Y : C} (φ : W.RightFraction X Y) : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)
    where
  Y' := Opposite.op φ.X'
  s := φ.s.op
  hs := φ.hs
  f := φ.f.op

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