English
The forgetful functor from CommRingCat to RingCat creates limits.
Русский
Функтор забывания из CommRingCat в RingCat создаёт пределы.
LaTeX
$$$\text{CommRingCat.instCreatesLimitRingCatForget₂}:\text{ CreatesLimit } F (\mathrm{forget}_2\ CommRingCat\, RingCat)$$$
Lean4
/-- We show that the forgetful functor `CommRingCat ⥤ RingCat` creates limits.
All we need to do is notice that the limit point has a `CommRing` instance available,
and then reuse the existing limit.
-/
instance : CreatesLimit F (forget₂ CommRingCat.{u} RingCat.{u}) :=
/-
A terse solution here would be
```
createsLimitOfFullyFaithfulOfIso (CommRingCat.of (limit (F ⋙ forget _))) (Iso.refl _)
```
but it seems this would introduce additional identity morphisms in `limit.π`.
-/
-- Porting note: need to add these instances manually
have : (forget₂ CommRingCat.{u} RingCat.{u}).ReflectsIsomorphisms := CategoryTheory.reflectsIsomorphisms_forget₂ _ _
have : Small.{u} (Functor.sections ((F ⋙ forget₂ CommRingCat RingCat) ⋙ forget RingCat)) :=
inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget _))
let F' := F ⋙ forget₂ CommRingCat.{u} RingCat.{u} ⋙ forget₂ RingCat.{u} SemiRingCat.{u}
have : Small.{u} (Functor.sections (F' ⋙ forget _)) := inferInstanceAs <| Small.{u} (F ⋙ forget _).sections
let c : Cone F :=
{ pt := CommRingCat.of (Types.Small.limitCone (F ⋙ forget _)).pt
π :=
{ app := fun x => ofHom <| SemiRingCat.limitπRingHom.{v, u} F' x
naturality := fun _ _ f =>
hom_ext <| RingHom.coe_inj ((Types.Small.limitCone (F ⋙ forget _)).π.naturality f) } }
createsLimitOfReflectsIso fun _ t =>
{ liftedCone := c
validLift := IsLimit.uniqueUpToIso (RingCat.limitConeIsLimit.{v, u} _) t
makesLimit :=
IsLimit.ofFaithful (forget₂ _ RingCat.{u})
(RingCat.limitConeIsLimit.{v, u} (F ⋙ forget₂ CommRingCat.{u} RingCat.{u}))
(fun s : Cone F =>
CommRingCat.ofHom <|
(RingCat.limitConeIsLimit.{v, u} (F ⋙ forget₂ CommRingCat.{u} RingCat.{u})).lift
((forget₂ _ RingCat.{u}).mapCone s) |>.hom)
fun _ => rfl }
