English
For left fractions z1,z2,z3 with a compatibility equation h3, under L, the equality z1.map ≫ z2.map = (z1.comp₀ z2 z3).map holds after localization.
Русский
Для левых дробей z1,z2,z3 со сходным условием h3, после локализации выполняется равенство $z_1.map ≫ z_2.map = (z_1.comp₀ z_2 z_3).map$.
LaTeX
$$$\forall {X Y Z : C} (z_1 : W.LeftFraction X Y) (z_2 : W.LeftFraction Y Z) (z_3 : W.LeftFraction z_1.Y' z_2.Y') (h_3 : z_2.f \;≫\; z_3.s = z_1.s \;≫\; z_3.f) (L : C \to D) [L.IsLocalization W],
z_1.map L (Localization.inverts L W) \;≫\; z_2.map L (Localization.inverts L W) =
(z_1.comp₀ z_2 z_3).map L (Localization.inverts L W)$$$
Lean4
theorem map_comp_map_eq_map {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) (L : C ⥤ D) [L.IsLocalization W] :
z₁.map L (Localization.inverts L W) ≫ z₂.map L (Localization.inverts L W) =
(z₁.comp₀ z₂ z₃).map L (Localization.inverts L W) :=
by
have := Localization.inverts L W _ z₂.hs
have := Localization.inverts L W _ z₃.hs
have : IsIso (L.map (z₂.s ≫ z₃.s)) := by
rw [L.map_comp]
infer_instance
dsimp [LeftFraction.comp₀]
rw [← cancel_mono (L.map (z₂.s ≫ z₃.s)), map_comp_map_s, L.map_comp, assoc, map_comp_map_s_assoc, ← L.map_comp, h₃,
L.map_comp, map_comp_map_s_assoc, L.map_comp]
