createsLimit — Mathlib

English

The forgetful functor GrpCat → MonCat creates limits; limits in GrpCat are obtained by transporting the limit from MonCat and equipping it with a compatible group structure.

Русский

Забывающий функтор GrpCat → MonCat создаёт пределы; пределы в GrpCat получаются путём переноса предела из MonCat и добавления совместной структуры группы.

LaTeX

$$$\\text{GrpCat.Forget₂}.createsLimit$$$

Lean4

/-- We show that the forgetful functor `GrpCat ⥤ MonCat` creates limits.

All we need to do is notice that the limit point has a `Group` instance available, and then reuse
the existing limit. -/
@[to_additive /-- We show that the forgetful functor `AddGrpCat ⥤ AddMonCat` creates limits.

    All we need to do is notice that the limit point has an `AddGroup` instance available, and then
    reuse the existing limit. -/
    ]
noncomputable instance createsLimit : CreatesLimit F (forget₂ GrpCat.{u} MonCat.{u}) :=
  -- Porting note: need to add `forget₂ GrpCat MonCat` reflects isomorphism

  letI : (forget₂ GrpCat.{u} MonCat.{u}).ReflectsIsomorphisms := CategoryTheory.reflectsIsomorphisms_forget₂ _ _
  createsLimitOfReflectsIso (K := F) (F := (forget₂ GrpCat.{u} MonCat.{u})) fun c' t =>
    have : Small.{u} (Functor.sections ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat)) :=
      by
      have : HasLimit (F ⋙ forget₂ GrpCat MonCat) := ⟨_, t⟩
      apply Concrete.small_sections_of_hasLimit (F ⋙ forget₂ GrpCat MonCat)
    have : Small.{u} (Functor.sections (F ⋙ forget GrpCat)) :=
      inferInstanceAs <| Small.{u} (Functor.sections ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat))
    { liftedCone :=
        { pt := GrpCat.of (Types.Small.limitCone (F ⋙ forget GrpCat)).pt
          π :=
            { app j := ofHom <| MonCat.limitπMonoidHom (F ⋙ forget₂ GrpCat MonCat) j
              naturality i j
                h :=
                hom_ext <|
                  congr_arg MonCat.Hom.hom <|
                    (MonCat.HasLimits.limitCone (F ⋙ forget₂ GrpCat MonCat.{u})).π.naturality h } }
      validLift := by apply IsLimit.uniqueUpToIso (MonCat.HasLimits.limitConeIsLimit.{v, u} _) t
      makesLimit :=
        IsLimit.ofFaithful (forget₂ GrpCat MonCat.{u}) (MonCat.HasLimits.limitConeIsLimit _) (fun _ => _) fun _ => rfl }

Похожие утверждения