Ulift

📁 Source: Mathlib/Algebra/Category/Grp/Ulift.lean

Statistics

Metric	Count
Definitions instCreatesColimitsOfSizeUliftFunctor, instCreatesLimitsOfSizeUliftFunctor, uliftFunctorFullyFaithful, instCreatesLimitsOfSizeUliftFunctor, uliftFunctorFullyFaithful, instCreatesLimitsOfSizeUliftFunctor, uliftFunctorFullyFaithful, instCreatesLimitsOfSizeUliftFunctor, uliftFunctorFullyFaithful	9
Theorems instFaithfulUliftFunctor, instFullUliftFunctor, instPreservesColimitsOfSizeUliftFunctor, uliftFunctor_additive, uliftFunctor_preservesLimit, uliftFunctor_preservesLimitsOfShape, uliftFunctor_preservesLimitsOfSize, instFaithfulUliftFunctor, instFullUliftFunctor, uliftFunctor_preservesLimit, uliftFunctor_preservesLimitsOfShape, uliftFunctor_preservesLimitsOfSize, instFaithfulUliftFunctor, instFullUliftFunctor, uliftFunctor_preservesLimit, uliftFunctor_preservesLimitsOfShape, uliftFunctor_preservesLimitsOfSize, instFaithfulUliftFunctor, instFullUliftFunctor, uliftFunctor_preservesLimit, uliftFunctor_preservesLimitsOfShape, uliftFunctor_preservesLimitsOfSize	22
Total	31

AddCommGrpCat

Definitions

Name	Category	Theorems
instCreatesColimitsOfSizeUliftFunctor 📖	CompOp	—
instCreatesLimitsOfSizeUliftFunctor 📖	CompOp	—
uliftFunctorFullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Faithful AddCommGrpCat instCategory uliftFunctor	—	CategoryTheory.Functor.FullyFaithful.faithful
instFullUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Full AddCommGrpCat instCategory uliftFunctor	—	CategoryTheory.Functor.FullyFaithful.full
instPreservesColimitsOfSizeUliftFunctor 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize AddCommGrpCat instCategory uliftFunctor	—	isColimit_iff_bijective_desc Function.Bijective.of_comp_iff AddEquiv.bijective AddEquiv.coe_toAddMonoidHom AddMonoidHom.coe_comp Colimits.Quot.desc_quotQuotUliftAddEquiv Function.Bijective.comp ULift.up_bijective
uliftFunctor_additive 📖	mathematical	—	CategoryTheory.Functor.Additive AddCommGrpCat instCategory instPreadditive uliftFunctor	—	—
uliftFunctor_preservesLimit 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AddCommGrpCat instCategory uliftFunctor	—	CategoryTheory.Functor.corepresentable_preservesLimit forget_isCorepresentable CategoryTheory.preservesLimit_comp_of_createsLimit CategoryTheory.Limits.comp_preservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.Types.instPreservesLimitsOfSizeUliftFunctor CategoryTheory.CreatesLimit.toReflectsLimit
uliftFunctor_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape AddCommGrpCat instCategory uliftFunctor	—	uliftFunctor_preservesLimit
uliftFunctor_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize AddCommGrpCat instCategory uliftFunctor	—	uliftFunctor_preservesLimitsOfShape

AddGrpCat

Definitions

Name	Category	Theorems
instCreatesLimitsOfSizeUliftFunctor 📖	CompOp	—
uliftFunctorFullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Faithful AddGrpCat instCategory uliftFunctor	—	CategoryTheory.Functor.FullyFaithful.faithful
instFullUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Full AddGrpCat instCategory uliftFunctor	—	CategoryTheory.Functor.FullyFaithful.full
uliftFunctor_preservesLimit 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AddGrpCat instCategory uliftFunctor	—	CategoryTheory.Functor.corepresentable_preservesLimit forget_isCorepresentable CategoryTheory.preservesLimit_comp_of_createsLimit CategoryTheory.Limits.comp_preservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.Types.instPreservesLimitsOfSizeUliftFunctor CategoryTheory.CreatesLimit.toReflectsLimit
uliftFunctor_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape AddGrpCat instCategory uliftFunctor	—	uliftFunctor_preservesLimit
uliftFunctor_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize AddGrpCat instCategory uliftFunctor	—	uliftFunctor_preservesLimitsOfShape

CommGrpCat

Definitions

Name	Category	Theorems
instCreatesLimitsOfSizeUliftFunctor 📖	CompOp	—
uliftFunctorFullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Faithful CommGrpCat instCategory uliftFunctor	—	CategoryTheory.Functor.FullyFaithful.faithful
instFullUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Full CommGrpCat instCategory uliftFunctor	—	CategoryTheory.Functor.FullyFaithful.full
uliftFunctor_preservesLimit 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CommGrpCat instCategory uliftFunctor	—	CategoryTheory.Functor.corepresentable_preservesLimit forget_isCorepresentable CategoryTheory.preservesLimit_comp_of_createsLimit CategoryTheory.Limits.comp_preservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.Types.instPreservesLimitsOfSizeUliftFunctor CategoryTheory.CreatesLimit.toReflectsLimit
uliftFunctor_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CommGrpCat instCategory uliftFunctor	—	uliftFunctor_preservesLimit
uliftFunctor_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize CommGrpCat instCategory uliftFunctor	—	uliftFunctor_preservesLimitsOfShape

GrpCat

Definitions

Name	Category	Theorems
instCreatesLimitsOfSizeUliftFunctor 📖	CompOp	—
uliftFunctorFullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Faithful GrpCat instCategory uliftFunctor	—	CategoryTheory.Functor.FullyFaithful.faithful
instFullUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Full GrpCat instCategory uliftFunctor	—	CategoryTheory.Functor.FullyFaithful.full
uliftFunctor_preservesLimit 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit GrpCat instCategory uliftFunctor	—	CategoryTheory.Functor.corepresentable_preservesLimit forget_isCorepresentable CategoryTheory.preservesLimit_comp_of_createsLimit CategoryTheory.Limits.comp_preservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.Types.instPreservesLimitsOfSizeUliftFunctor CategoryTheory.CreatesLimit.toReflectsLimit
uliftFunctor_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape GrpCat instCategory uliftFunctor	—	uliftFunctor_preservesLimit
uliftFunctor_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize GrpCat instCategory uliftFunctor	—	uliftFunctor_preservesLimitsOfShape

---

← Back to Index