Lemmas on fractions

Let W : MorphismProperty C, and objects X and Y in C. In this file, we introduce structures like W.LeftFraction₂ X Y which consists of two left fractions with the "same denominator" which shall be important in the construction of the preadditive structure on the localized category when C is preadditive and W has a left calculus of fractions.

When W has a left calculus of fractions, we generalize the lemmas RightFraction.exists_leftFraction as RightFraction₂.exists_leftFraction₂, Localization.exists_leftFraction as Localization.exists_leftFraction₂ and Localization.exists_leftFraction₃, and LeftFraction.map_eq_iff as LeftFraction₂.map_eq_iff.

Implementation note

The lemmas in this file are phrased with data that is bundled into structures like LeftFraction₂ or LeftFraction₃. It could have been possible to phrase them with "unbundled data". However, this would require introducing 4 or 5 variables instead of one. It is also very convenient to use dot notation. Many definitions have been made reducible so as to ease rewrites when this API is used.

structure CategoryTheory.MorphismProperty.LeftFraction₂ {C : Type u_1} [Category.{u_3, u_1} C] (W : MorphismProperty C) (X Y : C) : Type (max u_1 u_3)

This structure contains the data of two left fractions for W : MorphismProperty C that have the same "denominator".

• Y' : C

  the auxiliary object of left fractions

• f : X ⟶ self.Y'

  the numerator of the first left fraction

• f' : X ⟶ self.Y'

  the numerator of the second left fraction

• s : Y ⟶ self.Y'

  the denominator of the left fractions

• hs : W self.s

  the condition that the denominator belongs to the given morphism property

structure CategoryTheory.MorphismProperty.LeftFraction₃ {C : Type u_1} [Category.{u_3, u_1} C] (W : MorphismProperty C) (X Y : C) : Type (max u_1 u_3)

This structure contains the data of three left fractions for W : MorphismProperty C that have the same "denominator".

• Y' : C

  the auxiliary object of left fractions

• f : X ⟶ self.Y'

  the numerator of the first left fraction

• f' : X ⟶ self.Y'

  the numerator of the second left fraction

• f'' : X ⟶ self.Y'

  the numerator of the third left fraction

• s : Y ⟶ self.Y'

  the denominator of the left fractions

• hs : W self.s

  the condition that the denominator belongs to the given morphism property

structure CategoryTheory.MorphismProperty.RightFraction₂ {C : Type u_1} [Category.{u_3, u_1} C] (W : MorphismProperty C) (X Y : C) : Type (max u_1 u_3)

This structure contains the data of two right fractions for W : MorphismProperty C that have the same "denominator".

• X' : C

  the auxiliary object of right fractions

• s : self.X' ⟶ X

  the denominator of the right fractions

• hs : W self.s

  the condition that the denominator belongs to the given morphism property

• f : self.X' ⟶ Y

  the numerator of the first right fraction

• f' : self.X' ⟶ Y

  the numerator of the second right fraction

def CategoryTheory.MorphismProperty.LeftFraction₂Rel {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} {X Y : C} (z₁ z₂ : W.LeftFraction₂ X Y) : Prop

The equivalence relation on tuples of left fractions with the same denominator for a morphism property W. The fact it is an equivalence relation is not formalized, but it would follow easily from LeftFraction₂.map_eq_iff.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.LeftFraction₂.fst {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} {X Y : C} (φ : W.LeftFraction₂ X Y) : W.LeftFraction X Y

The first left fraction.

Equations

• φ.fst = CategoryTheory.MorphismProperty.LeftFraction.mk φ.f φ.s ⋯

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.LeftFraction₂.snd {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} {X Y : C} (φ : W.LeftFraction₂ X Y) : W.LeftFraction X Y

The second left fraction.

Equations

• φ.snd = CategoryTheory.MorphismProperty.LeftFraction.mk φ.f' φ.s ⋯

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.LeftFraction₂.symm {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} {X Y : C} (φ : W.LeftFraction₂ X Y) : W.LeftFraction₂ X Y

The exchange of the two fractions.

Equations

• φ.symm = CategoryTheory.MorphismProperty.LeftFraction₂.mk φ.f' φ.f φ.s ⋯

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.LeftFraction₃.fst {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} {X Y : C} (φ : W.LeftFraction₃ X Y) : W.LeftFraction X Y

The first left fraction.

Equations

• φ.fst = CategoryTheory.MorphismProperty.LeftFraction.mk φ.f φ.s ⋯

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.LeftFraction₃.snd {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} {X Y : C} (φ : W.LeftFraction₃ X Y) : W.LeftFraction X Y

The second left fraction.

Equations

• φ.snd = CategoryTheory.MorphismProperty.LeftFraction.mk φ.f' φ.s ⋯

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.LeftFraction₃.thd {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} {X Y : C} (φ : W.LeftFraction₃ X Y) : W.LeftFraction X Y

The third left fraction.

Equations

• φ.thd = CategoryTheory.MorphismProperty.LeftFraction.mk φ.f'' φ.s ⋯

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.LeftFraction₃.forgetFst {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} {X Y : C} (φ : W.LeftFraction₃ X Y) : W.LeftFraction₂ X Y

Forgets the first fraction.

Equations

• φ.forgetFst = CategoryTheory.MorphismProperty.LeftFraction₂.mk φ.f' φ.f'' φ.s ⋯

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.LeftFraction₃.forgetSnd {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} {X Y : C} (φ : W.LeftFraction₃ X Y) : W.LeftFraction₂ X Y

Forgets the second fraction.

Equations

• φ.forgetSnd = CategoryTheory.MorphismProperty.LeftFraction₂.mk φ.f φ.f'' φ.s ⋯

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.LeftFraction₃.forgetThd {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} {X Y : C} (φ : W.LeftFraction₃ X Y) : W.LeftFraction₂ X Y

Forgets the third fraction.

Equations

• φ.forgetThd = CategoryTheory.MorphismProperty.LeftFraction₂.mk φ.f φ.f' φ.s ⋯

theorem CategoryTheory.MorphismProperty.LeftFraction₂Rel.fst {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} {X Y : C} {z₁ z₂ : W.LeftFraction₂ X Y} (h : LeftFraction₂Rel z₁ z₂) : LeftFractionRel z₁.fst z₂.fst

theorem CategoryTheory.MorphismProperty.LeftFraction₂Rel.snd {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} {X Y : C} {z₁ z₂ : W.LeftFraction₂ X Y} (h : LeftFraction₂Rel z₁ z₂) : LeftFractionRel z₁.snd z₂.snd

theorem CategoryTheory.MorphismProperty.LeftFraction₂.map_eq_iff {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (φ ψ : W.LeftFraction₂ X Y) : φ.fst.map L ⋯ = ψ.fst.map L ⋯ ∧ φ.snd.map L ⋯ = ψ.snd.map L ⋯ ↔ LeftFraction₂Rel φ ψ

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.RightFraction₂.fst {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} {X Y : C} (φ : W.RightFraction₂ X Y) : W.RightFraction X Y

The first right fraction.

Equations

• φ.fst = CategoryTheory.MorphismProperty.RightFraction.mk φ.s ⋯ φ.f

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.RightFraction₂.snd {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} {X Y : C} (φ : W.RightFraction₂ X Y) : W.RightFraction X Y

The second right fraction.

Equations

• φ.snd = CategoryTheory.MorphismProperty.RightFraction.mk φ.s ⋯ φ.f'

theorem CategoryTheory.MorphismProperty.RightFraction₂.exists_leftFraction₂ {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} {X Y : C} (φ : W.RightFraction₂ X Y) [W.HasLeftCalculusOfFractions] : ∃ (ψ : W.LeftFraction₂ X Y), CategoryStruct.comp φ.f ψ.s = CategoryStruct.comp φ.s ψ.f ∧ CategoryStruct.comp φ.f' ψ.s = CategoryStruct.comp φ.s ψ.f'

theorem CategoryTheory.Localization.exists_leftFraction₂ {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f f' : L.obj X ⟶ L.obj Y) : ∃ (φ : W.LeftFraction₂ X Y), f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯

theorem CategoryTheory.Localization.exists_leftFraction₃ {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f f' f'' : L.obj X ⟶ L.obj Y) : ∃ (φ : W.LeftFraction₃ X Y), f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯