English
There exists a LeftFraction₂ realizing given pair of arrows after localization.
Русский
Существует LeftFraction₂, реализующий заданную пару стрелок после локализации.
LaTeX
$$$\\exists φ : W.LeftFraction₂ X Y, f = φ.fst.map L (inverts L W) \\land f' = φ.snd.map L (inverts L W)$$$
Lean4
theorem exists_leftFraction₃ {X Y : C} (f f' f'' : L.obj X ⟶ L.obj Y) :
∃ (φ : W.LeftFraction₃ X Y),
f = φ.fst.map L (inverts L W) ∧ f' = φ.snd.map L (inverts L W) ∧ f'' = φ.thd.map L (inverts L W) :=
by
obtain ⟨α, hα, hα'⟩ := exists_leftFraction₂ L W f f'
have ⟨β, hβ⟩ := exists_leftFraction L W f''
obtain ⟨γ, hγ⟩ := (RightFraction.mk _ α.hs β.s).exists_leftFraction
dsimp at hγ
let ψ : W.LeftFraction₃ X Y :=
{ Y' := γ.Y'
f := α.f ≫ γ.f
f' := α.f' ≫ γ.f
f'' := β.f ≫ γ.s
s := β.s ≫ γ.s
hs := W.comp_mem _ _ β.hs γ.hs }
have := inverts L W _ β.hs
have := inverts L W _ γ.hs
have : IsIso (L.map (β.s ≫ γ.s)) := by
rw [L.map_comp]
infer_instance
refine ⟨ψ, ?_, ?_, ?_⟩
·
rw [← cancel_mono (L.map (β.s ≫ γ.s)), LeftFraction.map_comp_map_s, hα, hγ, L.map_comp,
LeftFraction.map_comp_map_s_assoc, L.map_comp]
·
rw [← cancel_mono (L.map (β.s ≫ γ.s)), LeftFraction.map_comp_map_s, hα', hγ, L.map_comp,
LeftFraction.map_comp_map_s_assoc, L.map_comp]
· rw [← cancel_mono (L.map (β.s ≫ γ.s)), hβ]
nth_rw 1 [L.map_comp]
rw [LeftFraction.map_comp_map_s_assoc, LeftFraction.map_comp_map_s, L.map_comp]
