English
The forgetful functor Forget₂ from CommGrpCat to GrpCat preserves and reflects structure; it is compatible with forgetful constructions.
Русский
Забывающий функтор Forget₂ из CommGrpCat в GrpCat сохраняет и отражает структуру; совместим с забыванием.
LaTeX
$$$ (\mathrm{forget₂} \; CommGrpCat GrpCat) \text{ preserves and reflects structure} $$$
Lean4
/-- We show that the forgetful functor `CommGrpCat ⥤ GrpCat` creates limits.
All we need to do is notice that the limit point has a `CommGroup` instance available,
and then reuse the existing limit.
-/
@[to_additive /-- We show that the forgetful functor `AddCommGrpCat ⥤ AddGrpCat` creates limits.
All we need to do is notice that the limit point has an `AddCommGroup` instance available,
and then reuse the existing limit. -/
]
noncomputable instance createsLimit : CreatesLimit F (forget₂ CommGrpCat GrpCat.{u}) :=
createsLimitOfReflectsIso
(fun c hc => by
have : HasLimit _ := ⟨_, hc⟩
have : Small.{u} (F ⋙ forget CommGrpCat).sections :=
Concrete.small_sections_of_hasLimit (F ⋙ forget₂ CommGrpCat GrpCat)
have : Small.{u} ((F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).sections := this
have : Small.{u} ((F ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget GrpCat).sections := this
exact
{ liftedCone :=
{ pt := CommGrpCat.of (Types.Small.limitCone.{v, u} (F ⋙ forget CommGrpCat)).pt
π :=
{ app
j :=
ofHom <| MonCat.limitπMonoidHom (F ⋙ forget₂ CommGrpCat GrpCat.{u} ⋙ forget₂ GrpCat MonCat.{u}) j
naturality i j
h := hom_ext <| congr_arg MonCat.Hom.hom <| (MonCat.HasLimits.limitCone _).π.naturality h } }
validLift := by apply IsLimit.uniqueUpToIso (GrpCat.limitConeIsLimit _) hc
makesLimit :=
IsLimit.ofFaithful (forget₂ _ GrpCat.{u} ⋙ forget₂ _ MonCat.{u})
(by apply MonCat.HasLimits.limitConeIsLimit _) (fun s => _) fun s => rfl })
