Lean4
/-- 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₁ : Hom W X Y) (z₂ : Hom W Y Z) : Hom W X Z :=
by
refine Quot.lift₂ (fun a b => a.comp b) ?_ ?_ z₁ z₂
· rintro a b₁ b₂ ⟨U, t₁, t₂, hst, hft, ht⟩
obtain ⟨z₁, fac₁⟩ := exists_leftFraction (RightFraction.mk a.s a.hs b₁.f)
obtain ⟨z₂, fac₂⟩ := exists_leftFraction (RightFraction.mk a.s a.hs b₂.f)
obtain ⟨w₁, fac₁'⟩ := exists_leftFraction (RightFraction.mk z₁.s z₁.hs t₁)
obtain ⟨w₂, fac₂'⟩ := exists_leftFraction (RightFraction.mk z₂.s z₂.hs t₂)
obtain ⟨u, fac₃⟩ := exists_leftFraction (RightFraction.mk w₁.s w₁.hs w₂.s)
dsimp at fac₁ fac₂ fac₁' fac₂' fac₃ ⊢
have eq : a.s ≫ z₁.f ≫ w₁.f ≫ u.f = a.s ≫ z₂.f ≫ w₂.f ≫ u.s := by
rw [← reassoc_of% fac₁, ← reassoc_of% fac₂, ← reassoc_of% fac₁', ← reassoc_of% fac₂', reassoc_of% hft, fac₃]
obtain ⟨Z, p, hp, fac₄⟩ := HasLeftCalculusOfFractions.ext _ _ _ a.hs eq
simp only [assoc] at fac₄
rw [comp_eq _ _ z₁ fac₁, comp_eq _ _ z₂ fac₂]
apply Quot.sound
refine ⟨Z, w₁.f ≫ u.f ≫ p, w₂.f ≫ u.s ≫ p, ?_, ?_, ?_⟩
· dsimp
simp only [assoc, ← reassoc_of% fac₁', ← reassoc_of% fac₂', reassoc_of% hst, reassoc_of% fac₃]
· dsimp
simp only [assoc, fac₄]
· dsimp
simp only [assoc]
rw [← reassoc_of% fac₁', ← reassoc_of% fac₃, ← assoc]
exact W.comp_mem _ _ ht (W.comp_mem _ _ w₂.hs (W.comp_mem _ _ u.hs hp))
· rintro a₁ a₂ b ⟨U, t₁, t₂, hst, hft, ht⟩
obtain ⟨z₁, fac₁⟩ := exists_leftFraction (RightFraction.mk a₁.s a₁.hs b.f)
obtain ⟨z₂, fac₂⟩ := exists_leftFraction (RightFraction.mk a₂.s a₂.hs b.f)
obtain ⟨w₁, fac₁'⟩ := exists_leftFraction (RightFraction.mk (a₁.s ≫ t₁) ht (b.f ≫ z₁.s))
obtain ⟨w₂, fac₂'⟩ :=
exists_leftFraction (RightFraction.mk (a₂.s ≫ t₂) (show W _ by rw [← hst]; exact ht) (b.f ≫ z₂.s))
let p₁ : W.LeftFraction X Z :=
LeftFraction.mk (a₁.f ≫ t₁ ≫ w₁.f) (b.s ≫ z₁.s ≫ w₁.s) (W.comp_mem _ _ b.hs (W.comp_mem _ _ z₁.hs w₁.hs))
let p₂ : W.LeftFraction X Z :=
LeftFraction.mk (a₂.f ≫ t₂ ≫ w₂.f) (b.s ≫ z₂.s ≫ w₂.s) (W.comp_mem _ _ b.hs (W.comp_mem _ _ z₂.hs w₂.hs))
dsimp at fac₁ fac₂ fac₁' fac₂' ⊢
simp only [assoc] at fac₁' fac₂'
rw [comp_eq _ _ z₁ fac₁, comp_eq _ _ z₂ fac₂]
apply Quot.sound
refine LeftFractionRel.trans ?_ ((?_ : LeftFractionRel p₁ p₂).trans ?_)
· have eq : a₁.s ≫ z₁.f ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f := by rw [← fac₁', reassoc_of% fac₁]
obtain ⟨Z, u, hu, fac₃⟩ := HasLeftCalculusOfFractions.ext _ _ _ a₁.hs eq
simp only [assoc] at fac₃
refine ⟨Z, w₁.s ≫ u, u, ?_, ?_, ?_⟩
· dsimp [p₁]
simp only [assoc]
· dsimp [p₁]
simp only [assoc, fac₃]
· dsimp
simp only [assoc]
exact W.comp_mem _ _ b.hs (W.comp_mem _ _ z₁.hs (W.comp_mem _ _ w₁.hs hu))
· obtain ⟨q, fac₃⟩ :=
exists_leftFraction (RightFraction.mk (z₁.s ≫ w₁.s) (W.comp_mem _ _ z₁.hs w₁.hs) (z₂.s ≫ w₂.s))
dsimp at fac₃
simp only [assoc] at fac₃
have eq : a₁.s ≫ t₁ ≫ w₁.f ≫ q.f = a₁.s ≫ t₁ ≫ w₂.f ≫ q.s := by
rw [← reassoc_of% fac₁', ← fac₃, reassoc_of% hst, reassoc_of% fac₂']
obtain ⟨Z, u, hu, fac₄⟩ := HasLeftCalculusOfFractions.ext _ _ _ a₁.hs eq
simp only [assoc] at fac₄
refine ⟨Z, q.f ≫ u, q.s ≫ u, ?_, ?_, ?_⟩
· simp only [p₁, p₂, assoc, reassoc_of% fac₃]
· rw [assoc, assoc, assoc, assoc, fac₄, reassoc_of% hft]
· simp only [p₁, assoc, ← reassoc_of% fac₃]
exact W.comp_mem _ _ b.hs (W.comp_mem _ _ z₂.hs (W.comp_mem _ _ w₂.hs (W.comp_mem _ _ q.hs hu)))
· have eq : a₂.s ≫ z₂.f ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f := by rw [← fac₂', reassoc_of% fac₂]
obtain ⟨Z, u, hu, fac₄⟩ := HasLeftCalculusOfFractions.ext _ _ _ a₂.hs eq
simp only [assoc] at fac₄
refine ⟨Z, u, w₂.s ≫ u, ?_, ?_, ?_⟩
· dsimp [p₁, p₂]
simp only [assoc]
· dsimp [p₁, p₂]
simp only [assoc, fac₄]
· dsimp [p₁, p₂]
simp only [assoc]
exact W.comp_mem _ _ b.hs (W.comp_mem _ _ z₂.hs (W.comp_mem _ _ w₂.hs hu))
