English
Given three arrows in a localization, one can factor them through a single left fraction.
Русский
Существуют три стрелы в локализации, через которые можно пропустить три стрелы через одну левую дробь.
LaTeX
$$$\\exists φ : W.LeftFraction₃ X Y,\\; φ.fst.map L (inverts L W) = f,\\; φ.snd.map L (inverts L W) = f',\\; φ.thd.map L (inverts L W) = f''$$$
Lean4
theorem exists_leftFraction₂ {X Y : C} (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) :=
by
have ⟨φ, hφ⟩ := exists_leftFraction L W f
have ⟨φ', hφ'⟩ := exists_leftFraction L W f'
obtain ⟨α, hα⟩ := (RightFraction.mk _ φ.hs φ'.s).exists_leftFraction
let ψ : W.LeftFraction₂ X Y :=
{ Y' := α.Y'
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α, L.map_comp, hφ,
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]
