add'_zero — Mathlib

English

In the dual setting, the right calculus of fractions exists for the inverse-image along G.

Русский

В двойственном контексте существует правый расчёт дробей для обратного изображения вдоль G.

LaTeX

$$$((\mathrm{isomorphisms}(C_2)).inverseImage G).HasRightCalculusOfFractions$$$

Lean4

theorem add'_zero (f : L.obj X ⟶ L.obj Y) : add' W f (L.map 0) = f :=
  by
  obtain ⟨α, hα⟩ := exists_leftFraction L W f
  rw [add'_eq W f (L.map 0) (LeftFraction₂.mk α.f 0 α.s α.hs) hα, hα]; swap
  · have := inverts L W _ α.hs
    rw [← cancel_mono (L.map α.s), ← L.map_comp, Limits.zero_comp, LeftFraction.map_comp_map_s]
  dsimp [LeftFraction₂.add]
  rw [add_zero]

Похожие утверждения