English
If α: F ⟶ G is an isomorphism, then precomposition preserves Van Kampen colimit structure.
Русский
Если α: F ⟶ G — изоморфизм, то предобразование сохраняет структуру колимита Ван-Кампена.
LaTeX
$$$[IsIso α] \\Rightarrow IsVanKampenColimit((\\mathrm{Cocones.precompose}(α)).{ }_{{}}\\!\\!\\!\\!.obj c)$$$
Lean4
theorem map_reflective {Gl : C ⥤ D} {Gr : D ⥤ C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful] {F : J ⥤ D}
{c : Cocone (F ⋙ Gr)} (H : IsUniversalColimit c)
[∀ X (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)]
[∀ X (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl] :
IsUniversalColimit (Gl.mapCocone c) :=
by
have := adj.rightAdjoint_preservesLimits
have : PreservesColimitsOfSize.{u', v'} Gl := adj.leftAdjoint_preservesColimits
intro F' c' α f h hα hc'
have : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt)) :=
⟨⟨_, isLimitPullbackConeMapOfIsLimit _ pullback.condition (IsPullback.of_hasPullback _ _).isLimit⟩⟩
let α' := α ≫ (Functor.associator _ _ _).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom
have hα' : NatTrans.Equifibered α' := hα.comp (NatTrans.equifibered_of_isIso _)
have hadj : ∀ X, Gl.map (adj.unit.app X) = inv (adj.counit.app _) :=
by
intro X
apply IsIso.eq_inv_of_inv_hom_id
exact adj.left_triangle_components _
haveI : ∀ X, IsIso (Gl.map (adj.unit.app X)) := by
simp_rw [hadj]
infer_instance
have hα'' : ∀ j, Gl.map (Gr.map <| α'.app j) = adj.counit.app _ ≫ α.app j :=
by
intro j
rw [← cancel_mono (adj.counit.app <| F.obj j)]
dsimp [α']
simp only [Category.comp_id, Adjunction.counit_naturality_assoc, Category.id_comp, Adjunction.counit_naturality,
Category.assoc, Functor.map_comp]
have hc'' : ∀ j, α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f := NatTrans.congr_app h
let β := isoWhiskerLeft F' (asIso adj.counit) ≪≫ F'.rightUnitor
let c'' : Cocone (F' ⋙ Gr) :=
by
refine
{ pt := pullback (Gr.map f) (adj.unit.app _)
ι :=
{ app := fun j ↦ pullback.lift (Gr.map <| c'.ι.app j) (Gr.map (α'.app j) ≫ c.ι.app j) ?_
naturality := ?_ } }
· rw [← Gr.map_comp, ← hc'']
erw [← adj.unit_naturality]
rw [Gl.map_comp, hα'']
dsimp
simp only [Category.assoc, Functor.map_comp, adj.right_triangle_components_assoc]
· intro i j g
dsimp [α']
ext
all_goals
simp only [Category.comp_id, Category.id_comp, Category.assoc, ← Functor.map_comp, pullback.lift_fst,
pullback.lift_snd, ← Functor.map_comp_assoc]
· congr 1
exact c'.w _
· rw [α.naturality_assoc]
dsimp
rw [adj.counit_naturality, ← Category.assoc, Gr.map_comp_assoc]
congr 1
exact c.w _
let cf : (Cocones.precompose β.hom).obj c' ⟶ Gl.mapCocone c'' :=
by
refine { hom := pullback.lift ?_ f ?_ ≫ (PreservesPullback.iso _ _ _).inv, w := ?_ }
· exact inv <| adj.counit.app c'.pt
· simp [← cancel_mono (adj.counit.app <| Gl.obj c.pt)]
· intro j
rw [← Category.assoc, Iso.comp_inv_eq]
ext
all_goals
simp only [c'', PreservesPullback.iso_hom_fst, PreservesPullback.iso_hom_snd, pullback.lift_fst,
pullback.lift_snd, Category.assoc, Functor.mapCocone_ι_app, ← Gl.map_comp]
· rw [IsIso.comp_inv_eq, adj.counit_naturality]
dsimp [β]
rw [Category.comp_id]
· rw [Gl.map_comp, hα'', Category.assoc, hc'']
dsimp [β]
rw [Category.comp_id, Category.assoc]
have : cf.hom ≫ (PreservesPullback.iso _ _ _).hom ≫ pullback.fst _ _ ≫ adj.counit.app _ = 𝟙 _ := by
simp only [cf, IsIso.inv_hom_id, Iso.inv_hom_id_assoc, Category.assoc, pullback.lift_fst_assoc]
have : IsIso cf := by
apply @Cocones.cocone_iso_of_hom_iso (i := ?_)
rw [← IsIso.eq_comp_inv] at this
rw [this]
infer_instance
have ⟨Hc''⟩ := H c'' (whiskerRight α' Gr) (pullback.snd _ _) ?_ (hα'.whiskerRight Gr) ?_
· exact ⟨IsColimit.precomposeHomEquiv β c' <| (isColimitOfPreserves Gl Hc'').ofIsoColimit (asIso cf).symm⟩
· ext j
dsimp [c'']
simp only [pullback.lift_snd]
· intro j
apply IsPullback.of_right _ _ (IsPullback.of_hasPullback _ _)
· dsimp [α', c'']
simp only [Category.comp_id, Category.id_comp, Category.assoc, Functor.map_comp, pullback.lift_fst]
rw [← Category.comp_id (Gr.map f)]
refine ((hc' j).map Gr).paste_vert (IsPullback.of_vert_isIso ⟨?_⟩)
rw [← adj.unit_naturality, Category.comp_id, ← Category.assoc, ←
Category.id_comp (Gr.map ((Gl.mapCocone c).ι.app j))]
congr 1
rw [← cancel_mono (Gr.map (adj.counit.app (F.obj j)))]
dsimp
simp only [Category.comp_id, Adjunction.right_triangle_components, Category.id_comp, Category.assoc]
· dsimp [c'']
simp only [pullback.lift_snd]
