English
The forgetful functor forget₂ from RingCat to SemiRingCat creates limits; i.e., given a diagram F: J ⥤ RingCat, limits can be computed by first forgetting to SemiRingCat and then taking the limit there, with a suitable ring structure recovered on the limit.
Русский
Забывающий funtor forget₂: RingCat → SemiRingCat создаёт пределы; пределы восстанавливаются через забывание до SemiRingCat и последующий предел, с корректной структурой кольца на пределе.
LaTeX
$$$\text{CreatesLimit } F (\mathrm{forget}_2 \mathrm{RingCat} \mathrm{SemiRingCat}).$$$
Lean4
/-- We show that the forgetful functor `CommRingCat ⥤ RingCat` creates limits.
All we need to do is notice that the limit point has a `Ring` instance available,
and then reuse the existing limit.
-/
instance : CreatesLimit F (forget₂ RingCat.{u} SemiRingCat.{u}) :=
have : (forget₂ RingCat SemiRingCat).ReflectsIsomorphisms := CategoryTheory.reflectsIsomorphisms_forget₂ _ _
have : Small.{u} (Functor.sections ((F ⋙ forget₂ _ SemiRingCat) ⋙ forget _)) :=
inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget _))
let c : Cone F :=
{ pt := RingCat.of (Types.Small.limitCone (F ⋙ forget _)).pt
π :=
{ app := fun x => ofHom <| SemiRingCat.limitπRingHom.{v, u} (F ⋙ forget₂ _ SemiRingCat) x
naturality := fun _ _ f =>
hom_ext <| RingHom.coe_inj ((Types.Small.limitCone (F ⋙ forget _)).π.naturality f) } }
createsLimitOfReflectsIso fun c' t =>
{ liftedCone := c
validLift := by apply IsLimit.uniqueUpToIso (SemiRingCat.HasLimits.limitConeIsLimit _) t
makesLimit :=
IsLimit.ofFaithful (forget₂ RingCat SemiRingCat.{u}) (by apply SemiRingCat.HasLimits.limitConeIsLimit _)
(fun _ => _) fun _ => rfl }
