Lean4
/-- If `L : C ⥤ D` is a localization functor for `W` and `e : F ≅ L ⋙ G` is an isomorphism,
then `e.hom` makes `G` a pointwise left Kan extension of `F` along `L` at `L.obj Y`
for any `Y : C`. -/
def isPointwiseLeftKanExtensionAtOfIsoOfIsLocalization {G : D ⥤ H} (e : F ≅ L ⋙ G) [L.IsLocalization W] (Y : C) :
(LeftExtension.mk _ e.hom).IsPointwiseLeftKanExtensionAt (L.obj Y)
where
desc s := e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))
fac s
j :=
by
refine Localization.induction_costructuredArrow L W _ (by simp) (fun X₁ X₂ f φ hφ ↦ ?_) (fun X₁ X₂ w hw φ hφ ↦ ?_) j
· have eq :=
s.ι.naturality (CostructuredArrow.homMk f : CostructuredArrow.mk (L.map f ≫ φ) ⟶ CostructuredArrow.mk φ)
dsimp at eq hφ ⊢
rw [comp_id] at eq
rw [assoc] at hφ
rw [assoc, map_comp_assoc, ← eq, ← hφ, NatTrans.naturality_assoc, comp_map]
· have : IsIso (F.map w) := by
have := Localization.inverts L W w hw
rw [← NatIso.naturality_2 e w]
dsimp
infer_instance
have eq :=
s.ι.naturality
(CostructuredArrow.homMk w :
CostructuredArrow.mk φ ⟶ CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ))
dsimp at eq hφ ⊢
rw [comp_id] at eq
rw [assoc] at hφ
rw [map_comp, assoc, assoc, ← cancel_epi (F.map w), eq, ← hφ, NatTrans.naturality_assoc, comp_map, ←
G.map_comp_assoc]
simp
uniq s m
hm := by
have := hm (CostructuredArrow.mk (𝟙 (L.obj Y)))
dsimp at this m hm ⊢
simp only [← this, map_id, comp_id, Iso.inv_hom_id_app_assoc]
