English
Composition distributes over the addition in the localized setting.
Русский
Сложение распространяется на композицию в локализации.
LaTeX
$$$f_1, f_2: X'\to Y',\ g: Y'\to Z',\; f_1 \;\text{comp} \; add\; f_2 \; g = add\; (f_1 \; g) \; (f_2 \; g)$$$
Lean4
@[reassoc (attr := simp)]
theorem comp_add' (f : L.obj X ⟶ L.obj Y) (g₁ g₂ : L.obj Y ⟶ L.obj Z) : f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂) :=
by
obtain ⟨α, hα⟩ := exists_leftFraction L W f
obtain ⟨β, hβ₁, hβ₂⟩ := exists_leftFraction₂ L W g₁ g₂
obtain ⟨γ, hγ₁, hγ₂⟩ := (RightFraction₂.mk _ α.hs β.f β.f').exists_leftFraction₂
dsimp at hγ₁ hγ₂
rw [add'_eq W g₁ g₂ β hβ₁ hβ₂,
add'_eq W (f ≫ g₁) (f ≫ g₂) (LeftFraction₂.mk (α.f ≫ γ.f) (α.f ≫ γ.f') (β.s ≫ γ.s) (W.comp_mem _ _ β.hs γ.hs))
(by simpa only [hα, hβ₁] using LeftFraction.map_comp_map_eq_map α β.fst γ.fst hγ₁ L)
(by simpa only [hα, hβ₂] using LeftFraction.map_comp_map_eq_map α β.snd γ.snd hγ₂ L),
hα, LeftFraction.map_comp_map_eq_map α β.add γ.add (by simp only [add_comp, hγ₁, hγ₂, comp_add])]
dsimp [LeftFraction₂.add]
rw [comp_add]
