Properties of the universe lift functor for groups

This file shows that the functors Grp.uliftFunctor and CommGrp.uliftFunctor (as well as the additive versions) are fully faithful, preserves all limits and create small limits.

It also shows that AddCommGrp.uliftFunctor is an additive functor.

def Grp.uliftFunctorFullyFaithful : Grp.uliftFunctor.FullyFaithful

The universe lift functor for groups is fully faithful.

Equations

• One or more equations did not get rendered due to their size.

def AddGrp.uliftFunctorFullyFaithful : AddGrp.uliftFunctor.FullyFaithful

The universe lift functor for additive groups is fully faithful.

Equations

• One or more equations did not get rendered due to their size.

instance Grp.instFaithfulUliftFunctor : Grp.uliftFunctor.Faithful

The universe lift functor for groups is faithful.

instance AddGrp.instFaithfulUliftFunctor : AddGrp.uliftFunctor.Faithful

The universe lift functor for additive groups is faithful.

instance Grp.instFullUliftFunctor : Grp.uliftFunctor.Full

The universe lift functor for groups is full.

instance AddGrp.instFullUliftFunctor : AddGrp.uliftFunctor.Full

The universe lift functor for additive groups is full.

instance Grp.uliftFunctor_preservesLimit {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Grp) : CategoryTheory.Limits.PreservesLimit K Grp.uliftFunctor

instance AddGrp.uliftFunctor_preservesLimit {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J AddGrp) : CategoryTheory.Limits.PreservesLimit K AddGrp.uliftFunctor

instance Grp.uliftFunctor_preservesLimitsOfShape {J : Type w} [CategoryTheory.Category.{w', w} J] : CategoryTheory.Limits.PreservesLimitsOfShape J Grp.uliftFunctor

instance AddGrp.uliftFunctor_preservesLimitsOfShape {J : Type w} [CategoryTheory.Category.{w', w} J] : CategoryTheory.Limits.PreservesLimitsOfShape J AddGrp.uliftFunctor

instance Grp.uliftFunctor_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} Grp.uliftFunctor

The universe lift for groups preserves limits of arbitrary size.

instance AddGrp.uliftFunctor_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} AddGrp.uliftFunctor

The universe lift functor for additive groups preserves limits of arbitrary size.

noncomputable instance Grp.instCreatesLimitsOfSizeUliftFunctor : CategoryTheory.CreatesLimitsOfSize.{w, u, u, max u v, u + 1, max (u + 1) (v + 1)} Grp.uliftFunctor

The universe lift functor on Grp.{u} creates u-small limits.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance AddGrp.instCreatesLimitsOfSizeUliftFunctor : CategoryTheory.CreatesLimitsOfSize.{w, u, u, max u v, u + 1, max (u + 1) (v + 1)} AddGrp.uliftFunctor

The universe lift functor on AddGrp.{u} creates u-small limits.

Equations

• One or more equations did not get rendered due to their size.

def CommGrp.uliftFunctorFullyFaithful : CommGrp.uliftFunctor.FullyFaithful

The universe lift functor for commutative groups is fully faithful.

Equations

• One or more equations did not get rendered due to their size.

def AddCommGrp.uliftFunctorFullyFaithful : AddCommGrp.uliftFunctor.FullyFaithful

The universe lift functor for commutative additive groups is fully faithful.

Equations

• One or more equations did not get rendered due to their size.

instance CommGrp.instFaithfulUliftFunctor : CommGrp.uliftFunctor.Faithful

instance AddCommGrp.instFaithfulUliftFunctor : AddCommGrp.uliftFunctor.Faithful

The universe lift functor for commutative additive groups is faithful.

instance CommGrp.instFullUliftFunctor : CommGrp.uliftFunctor.Full

instance AddCommGrp.instFullUliftFunctor : AddCommGrp.uliftFunctor.Full

The universe lift functor for commutative additive groups is full.

instance CommGrp.uliftFunctor_preservesLimit {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J CommGrp) : CategoryTheory.Limits.PreservesLimit K CommGrp.uliftFunctor

instance AddCommGrp.uliftFunctor_preservesLimit {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J AddCommGrp) : CategoryTheory.Limits.PreservesLimit K AddCommGrp.uliftFunctor

instance CommGrp.uliftFunctor_preservesLimitsOfShape {J : Type w} [CategoryTheory.Category.{w', w} J] : CategoryTheory.Limits.PreservesLimitsOfShape J CommGrp.uliftFunctor

instance AddCommGrp.uliftFunctor_preservesLimitsOfShape {J : Type w} [CategoryTheory.Category.{w', w} J] : CategoryTheory.Limits.PreservesLimitsOfShape J AddCommGrp.uliftFunctor

instance CommGrp.uliftFunctor_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} CommGrp.uliftFunctor

The universe lift for commutative groups preserves limits of arbitrary size.

instance AddCommGrp.uliftFunctor_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} AddCommGrp.uliftFunctor

The universe lift functor for commutative additive groups preserves limits of arbitrary size.

noncomputable instance CommGrp.instCreatesLimitsOfSizeUliftFunctor : CategoryTheory.CreatesLimitsOfSize.{w, u, u, max u v, u + 1, max (u + 1) (v + 1)} CommGrp.uliftFunctor

The universe lift functor on CommGrp.{u} creates u-small limits.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance AddCommGrp.instCreatesLimitsOfSizeUliftFunctor : CategoryTheory.CreatesLimitsOfSize.{w, u, u, max u v, u + 1, max (u + 1) (v + 1)} AddCommGrp.uliftFunctor

The universe lift functor on AddCommGrp.{u} creates u-small limits.

Equations

• One or more equations did not get rendered due to their size.

instance AddCommGroup.uliftFunctor_additive : AddCommGrp.uliftFunctor.Additive

The universe lift for commutative additive groups is additive.