English
The forgetful functor from CommSemiRingCat to SemiRingCat creates limits.
Русский
Забывающий функтор из CommSemiRingCat в SemiRingCat создаёт пределы.
LaTeX
$$$\operatorname{CreatesLimit}\big(F,\;\operatorname{forget}_2\, CommSemiRingCat\, SemiRingCat\big)$$$
Lean4
/-- We show that the forgetful functor `CommSemiRingCat ⥤ SemiRingCat` creates limits.
All we need to do is notice that the limit point has a `CommSemiring` instance available,
and then reuse the existing limit.
-/
instance : CreatesLimit F (forget₂ CommSemiRingCat.{u} SemiRingCat.{u}) :=
-- Porting note: Lean cannot see `CommSemiRingCat ⥤ SemiRingCat` reflects isomorphism, so this
-- instance is added.
let _ : (forget₂ CommSemiRingCat.{u} SemiRingCat.{u}).ReflectsIsomorphisms :=
CategoryTheory.reflectsIsomorphisms_forget₂ CommSemiRingCat.{u} SemiRingCat.{u}
let _ : Small.{u} (Functor.sections ((F ⋙ forget₂ _ SemiRingCat) ⋙ forget _)) :=
inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget CommSemiRingCat))
let c : Cone F :=
{ pt := CommSemiRingCat.of (Types.Small.limitCone (F ⋙ forget _)).pt
π :=
{ app := fun j =>
CommSemiRingCat.ofHom <|
SemiRingCat.limitπRingHom.{v, u} (J := J) (F ⋙ forget₂ CommSemiRingCat.{u} SemiRingCat.{u}) j
naturality := fun _ _ f ↦
hom_ext <|
congrArg SemiRingCat.Hom.hom <|
(SemiRingCat.HasLimits.limitCone.{v, u} (F ⋙ forget₂ CommSemiRingCat.{u} SemiRingCat.{u})).π.naturality
f } }
createsLimitOfReflectsIso fun c' t =>
{ liftedCone := c
validLift := IsLimit.uniqueUpToIso (SemiRingCat.HasLimits.limitConeIsLimit.{v, u} _) t
makesLimit := by
refine
IsLimit.ofFaithful (forget₂ CommSemiRingCat.{u} SemiRingCat.{u})
(SemiRingCat.HasLimits.limitConeIsLimit.{v, u} _) (fun s => _) fun s => rfl }
