Theorems · Inductive type · category theory

CategoryTheory.MorphismProperty.RightFraction

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.MorphismProperty C → C → C → Type (max u_1 v_1)

A right fraction from X : C to Y : C for W : MorphismProperty C consists of the datum of an object X' : C and maps s : X' ⟶ X and f : X' ⟶ Y such that W s.

Defined in

Mathlib.CategoryTheory.Localization.CalculusOfFractions

Cited by

37 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.Category