English
There exists a left calculus of fractions structure for a given adjunction with respect to W.
Русский
Существует структура левого исчисления дробей для данного сопряжения относительно W.
LaTeX
$$$\\text{hasLeftCalculusOfFractions}(adj,W)$$$
Lean4
theorem hasLeftCalculusOfFractions (adj : G ⊣ F) (W : MorphismProperty C₁) [W.IsMultiplicative] (hW : W.IsInvertedBy G)
(hW' : (W.functorCategory C₁) adj.unit) : W.HasLeftCalculusOfFractions
where
exists_leftFraction X Y
φ := by
obtain ⟨T, s, _, f, rfl⟩ := φ.cases
dsimp
have := hW s (by assumption)
exact
⟨{ f := adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)
s := adj.unit.app Y
hs := hW' Y }, by
have := adj.unit.naturality s
dsimp at this ⊢
rw [reassoc_of% this, Functor.map_inv, IsIso.hom_inv_id_assoc, adj.unit_naturality]⟩
ext X' X Y f₁ f₂ s _
h := by
have := hW s (by assumption)
refine ⟨_, adj.unit.app Y, hW' _, ?_⟩
rw [← adj.unit_naturality f₁, ← adj.unit_naturality f₂]
congr 2
rw [← cancel_epi (G.map s), ← G.map_comp, ← G.map_comp, h]
