Mathlib Map

Theorems · Definition · category theory

AddCommGrpCat.Colimits.quotQuotUliftAddEquiv

{J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      [inst_1 : DecidableEq J] →
        AddCommGrpCat.Colimits.Quot F ≃+ AddCommGrpCat.Colimits.Quot (F.comp AddCommGrpCat.uliftFunctor)

The additive equivalence between Quot F and Quot (F ⋙ uliftFunctor.{u'}).

Defined in
Mathlib.Algebra.Category.Grp.Colimits
Cited by
1 results in Mathlib
Foundations
Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.CategoryDecidableEq
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AddCommGrpCat.Colimits.Quot.desc_quotQuotUliftAddEquiv · cited by 0Quot.desc_quotQuotUliftAd…DFunLike.coe · cited by 62936DFunLike.coeCategoryTheory.Category · cited by 32673CategoryTheory.CategoryCategoryTheory.Functor · cited by 16252CategoryTheory.FunctorCategoryTheory.Functor.comp · cited by 6529Functor.compAddEquiv · cited by 1087AddEquivAddCommGrpCat · cited by 462AddCommGrpCatAddCommGrpCat.Colimits.Quot · cited by 16Colimits.QuotAddCommGrpCat.uliftFunctor · cited by 7AddCommGrpCat.uliftFunctorAddCommGrpCat.Colimits.quotToQuotUlift · cited by 1Colimits.quotToQuotUliftAddCommGrpCat.Colimits.quotUliftToQuot · cited by 1Colimits.quotUliftToQuotColimits.quotQuotUliftAddEquivCITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.