Theorems · Definition · category theory

CategoryTheory.MorphismProperty.LeftFraction.unop

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty Cᵒᵖ} →
      {X Y : Cᵒᵖ} → W.LeftFraction X Y → W.unop.RightFraction (Opposite.unop Y) (Opposite.unop X)

The right fraction corresponding to a left fraction in the opposite category.

Defined in: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Cited by: 5 results in Mathlib
Foundations: Depth 12 from the axioms · uses propext
Assumes: CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
Oppositestatement and proof · cited by 8,081
Opposite.unopstatement · cited by 2,231
CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
Quiver.Hom.unopproof · cited by 903
CategoryTheory.MorphismProperty.LeftFractionstatement and proof · cited by 67
CategoryTheory.MorphismProperty.LeftFraction.fproof · cited by 52
CategoryTheory.MorphismProperty.LeftFraction.sproof · cited by 51
CategoryTheory.MorphismProperty.RightFractionstatement · cited by 37
CategoryTheory.MorphismProperty.unopstatement · cited by 22

Cited by5

Results whose statement or proof uses this declaration.

CategoryTheory.Localization.exists_rightFractionproof · cited by 5
CategoryTheory.MorphismProperty.LeftFractionRel.unopstatement and proof · cited by 4
CategoryTheory.MorphismProperty.LeftFraction.unop_X'statement and proof · cited by 0
CategoryTheory.MorphismProperty.LeftFraction.unop_fstatement and proof · cited by 0
CategoryTheory.MorphismProperty.LeftFraction.unop_sstatement and proof · cited by 0