feat(CategoryTheory/Localization): equivalence relation on left fract…

…ions (#8055)

Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean

@@ -190,6 +190,149 @@ class HasRightCalculusOfFractions extends W.IsMultiplicative : Prop where
   ext : ∀ ⦃X Y Y' : C⦄ (f₁ f₂ : X ⟶ Y) (s : Y ⟶ Y') (_ : W s)
     (_ : f₁ ≫ s = f₂ ≫ s), ∃ (X' : C) (t : X' ⟶ X) (_ : W t), t ≫ f₁ = t ≫ f₂
 
+variable {W}
+
+lemma RightFraction.exists_leftFraction [W.HasLeftCalculusOfFractions] {X Y : C}
+    (φ : W.RightFraction X Y) : ∃ (ψ : W.LeftFraction X Y), φ.f ≫ ψ.s = φ.s ≫ ψ.f :=
+  HasLeftCalculusOfFractions.exists_leftFraction φ
+
+/-- A choice of a left fraction deduced from a right fraction for a morphism property `W`
+when `W` has left calculus of fractions. -/
+noncomputable def RightFraction.leftFraction [W.HasLeftCalculusOfFractions] {X Y : C}
+    (φ : W.RightFraction X Y) : W.LeftFraction X Y :=
+  φ.exists_leftFraction.choose
+
+@[reassoc]
+lemma RightFraction.leftFraction_fac [W.HasLeftCalculusOfFractions] {X Y : C}
+    (φ : W.RightFraction X Y) : φ.f ≫ φ.leftFraction.s = φ.s ≫ φ.leftFraction.f :=
+  φ.exists_leftFraction.choose_spec
+
+lemma LeftFraction.exists_rightFraction [W.HasRightCalculusOfFractions] {X Y : C}
+    (φ : W.LeftFraction X Y) : ∃ (ψ : W.RightFraction X Y), ψ.s ≫ φ.f = ψ.f ≫ φ.s :=
+  HasRightCalculusOfFractions.exists_rightFraction φ
+
+/-- A choice of a right fraction deduced from a left fraction for a morphism property `W`
+when `W` has right calculus of fractions. -/
+noncomputable def LeftFraction.rightFraction [W.HasRightCalculusOfFractions] {X Y : C}
+    (φ : W.LeftFraction X Y) : W.RightFraction X Y :=
+  φ.exists_rightFraction.choose
+
+@[reassoc]
+lemma LeftFraction.rightFraction_fac [W.HasRightCalculusOfFractions] {X Y : C}
+    (φ : W.LeftFraction X Y) : φ.rightFraction.s ≫ φ.f = φ.rightFraction.f ≫ φ.s :=
+  φ.exists_rightFraction.choose_spec
+
+/-- The equivalence relation on left fractions for a morphism property `W`. -/
+def LeftFractionRel {X Y : C} (z₁ z₂ : W.LeftFraction X Y) : Prop :=
+  ∃ (Z : C)  (t₁ : z₁.Y' ⟶ Z) (t₂ : z₂.Y' ⟶ Z) (_ : z₁.s ≫ t₁ = z₂.s ≫ t₂)
+    (_ : z₁.f ≫ t₁ = z₂.f ≫ t₂), W (z₁.s ≫ t₁)
+
+namespace LeftFractionRel
+
+lemma refl {X Y : C} (z : W.LeftFraction X Y) : LeftFractionRel z z :=
+  ⟨z.Y', 𝟙 _, 𝟙 _, rfl, rfl, by simpa only [Category.comp_id] using z.hs⟩
+
+lemma symm {X Y : C} {z₁ z₂ : W.LeftFraction X Y} (h : LeftFractionRel z₁ z₂) :
+    LeftFractionRel z₂ z₁ := by
+  obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h
+  exact ⟨Z, t₂, t₁, hst.symm, hft.symm, by simpa only [← hst] using ht⟩
+
+lemma trans {X Y : C} {z₁ z₂ z₃ : W.LeftFraction X Y}
+    [HasLeftCalculusOfFractions W]
+    (h₁₂ : LeftFractionRel z₁ z₂) (h₂₃ : LeftFractionRel z₂ z₃) :
+    LeftFractionRel z₁ z₃ := by
+  obtain ⟨Z₄, t₁, t₂, hst, hft, ht⟩ := h₁₂
+  obtain ⟨Z₅, u₂, u₃, hsu, hfu, hu⟩ := h₂₃
+  obtain ⟨⟨v₄, v₅, hv₅⟩, fac⟩ := HasLeftCalculusOfFractions.exists_leftFraction
+    (RightFraction.mk (z₁.s ≫ t₁) ht (z₃.s ≫ u₃))
+  simp only [Category.assoc] at fac
+  have eq : z₂.s ≫ u₂ ≫ v₅  = z₂.s ≫ t₂ ≫ v₄ := by
+    simpa only [← reassoc_of% hsu, reassoc_of% hst] using fac
+  obtain ⟨Z₇, w, hw, fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ z₂.hs eq
+  simp only [Category.assoc] at fac'
+  refine' ⟨Z₇, t₁ ≫ v₄ ≫ w, u₃ ≫ v₅ ≫ w, _, _, _⟩
+  · rw [reassoc_of% fac]
+  · rw [reassoc_of% hft, ← fac', reassoc_of% hfu]
+  · rw [← reassoc_of% fac, ← reassoc_of% hsu, ← Category.assoc]
+    exact W.comp_mem _ _ hu (W.comp_mem _ _ hv₅ hw)
+
+end LeftFractionRel
+
+section
+
+variable [W.HasLeftCalculusOfFractions] (W)
+
+lemma equivalenceLeftFractionRel (X Y : C) :
+    @_root_.Equivalence (W.LeftFraction X Y) LeftFractionRel where
+  refl := LeftFractionRel.refl
+  symm := LeftFractionRel.symm
+  trans := LeftFractionRel.trans
+
+variable {W}
+
+namespace LeftFraction
+
+/-- Auxiliary definition for the composition of left fractions. -/
+@[simp]
+def comp₀ {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z)
+    (z₃ : W.LeftFraction z₁.Y' z₂.Y') :
+    W.LeftFraction X Z :=
+  mk (z₁.f ≫ z₃.f) (z₂.s ≫ z₃.s) (W.comp_mem _ _ z₂.hs z₃.hs)
+
+/-- The equivalence class of `z₁.comp₀ z₂ z₃` does not depend on the choice of `z₃` provided
+they satisfy the compatibility `z₂.f ≫ z₃.s = z₁.s ≫ z₃.f`. -/
+lemma comp₀_rel {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z)
+    (z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y') (h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f)
+    (h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f) :
+    LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃') := by
+  obtain ⟨z₄, fac⟩ := HasLeftCalculusOfFractions.exists_leftFraction
+    (RightFraction.mk z₃.s z₃.hs z₃'.s)
+  dsimp at fac
+  have eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s := by
+    rw [← reassoc_of% h₃, ← reassoc_of% h₃', fac]
+  obtain ⟨Y, t, ht, fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ z₁.hs eq
+  simp only [assoc] at fac'
+  refine' ⟨Y, z₄.f ≫ t, z₄.s ≫ t, _, _, _⟩
+  · simp only [comp₀, assoc, reassoc_of% fac]
+  · simp only [comp₀, assoc, fac']
+  · simp only [comp₀, assoc, ← reassoc_of% fac]
+    exact W.comp_mem _ _ z₂.hs (W.comp_mem _ _ z₃'.hs (W.comp_mem _ _ z₄.hs ht))
+
+variable (W)
+
+/-- The morphisms in the constructed localized category for a morphism property `W`
+that has left calculus of fractions are equivalence classes of left fractions. -/
+def Localization.Hom (X Y : C) :=
+  Quot (LeftFractionRel : W.LeftFraction X Y → W.LeftFraction X Y → Prop)
+
+variable {W}
+
+/-- The morphism in the constructed localized category that is induced by a left fraction. -/
+def Localization.Hom.mk {X Y : C} (z : W.LeftFraction X Y) : Localization.Hom W X Y :=
+  Quot.mk _ z
+
+lemma Localization.Hom.mk_surjective {X Y : C} (f : Localization.Hom W X Y) :
+    ∃ (z : W.LeftFraction X Y), f = mk z := by
+  obtain ⟨z⟩ := f
+  exact ⟨z, rfl⟩
+
+/-- Auxiliary definition towards the definition of the composition of morphisms
+in the constructed localized category for a morphism property that has
+left calculus of fractions. -/
+noncomputable def comp {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z) :
+    Localization.Hom W X Z :=
+  Localization.Hom.mk (z₁.comp₀ z₂ (RightFraction.mk z₁.s z₁.hs z₂.f).leftFraction)
+
+lemma comp_eq {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z)
+    (z₃ : W.LeftFraction z₁.Y' z₂.Y') (h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f) :
+    z₁.comp z₂ = Localization.Hom.mk (z₁.comp₀ z₂ z₃) :=
+  Quot.sound (LeftFraction.comp₀_rel _ _ _ _
+    (RightFraction.leftFraction_fac (RightFraction.mk z₁.s z₁.hs z₂.f)) h₃)
+
+end LeftFraction
+
+end
+
 end MorphismProperty
 
 end CategoryTheory