Theorems · Definition · category theory

CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints

{M : Type v} →
  [inst : Monoid M] →
    (J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)) →
      ↑J.sections ≃ ↑(MulAction.fixedPoints M (J.obj (CategoryTheory.SingleObj.star M)))

The equivalence between sections of J : SingleObj M ⥤ Type u and fixed points of the induced action on J.obj (SingleObj.star M).

Defined in: Mathlib.CategoryTheory.Limits.Shapes.SingleObj
Cited by: 3 results in Mathlib
Foundations: Depth 17 from the axioms · uses propext, Quot.sound
Assumes: Monoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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

CategoryTheory.Functor.objstatement and proof · cited by 19,642
CategoryTheory.Functorstatement and proof · cited by 16,252
Equivstatement · cited by 8,337
Set.Elemstatement and proof · cited by 7,166
Monoidstatement and proof · cited by 3,887
CategoryTheory.Functor.sectionsstatement and proof · cited by 140
CategoryTheory.SingleObjstatement and proof · cited by 88
MulAction.fixedPointsstatement and proof · cited by 41
CategoryTheory.SingleObj.starstatement and proof · cited by 15

Cited by4

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPointsproof · cited by 2
CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints_symm_apply_coestatement and proof · cited by 0
CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints_symm_applystatement · cited by 0
CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints_apply_coestatement and proof · cited by 0