English
A left-adjoint-led localization for the inverse-image of isomorphisms exists, given an adjunction with G ⊣ F and the corresponding units are compatible.
Русский
Существует локализация слева, индуцированная левой сопряжённой связью при допустимой совместимости единиц.
LaTeX
$$$\mathrm{IsLocalization}(G, (\mathrm{isomorphisms}(C_2))^{-1}\!\text{-image } G)$$$
Lean4
theorem add'_eq (f₁ f₂ : L.obj X ⟶ L.obj Y) (φ : W.LeftFraction₂ X Y) (hφ₁ : f₁ = φ.fst.map L (inverts L W))
(hφ₂ : f₂ = φ.snd.map L (inverts L W)) : add' W f₁ f₂ = φ.add.map L (inverts L W) :=
by
obtain ⟨φ₀, rfl, rfl, hφ₀⟩ :
∃ (φ₀ : W.LeftFraction₂ X Y) (_ : f₁ = φ₀.fst.map L (inverts L W)) (_ : f₂ = φ₀.snd.map L (inverts L W)),
add' W f₁ f₂ = φ₀.add.map L (inverts L W) :=
⟨(exists_leftFraction₂ L W f₁ f₂).choose, (exists_leftFraction₂ L W f₁ f₂).choose_spec.1,
(exists_leftFraction₂ L W f₁ f₂).choose_spec.2, rfl⟩
obtain ⟨Z, t₁, t₂, hst, hft, hft', ht⟩ := (LeftFraction₂.map_eq_iff L W φ₀ φ).1 ⟨hφ₁, hφ₂⟩
have := inverts L W _ ht
rw [hφ₀, ← cancel_mono (L.map (φ₀.s ≫ t₁))]
nth_rw 2 [hst]
rw [L.map_comp, L.map_comp, LeftFraction.map_comp_map_s_assoc, LeftFraction.map_comp_map_s_assoc, ← L.map_comp, ←
L.map_comp, add_comp, add_comp, hft, hft']
