Documentation

Mathlib.RepresentationTheory.Action.Limits

Categorical properties of Action V G #

We show:

F : C ⥤ Action V G preserves the limit of some K : J ⥤ C if if it does after postcomposing with the forgetful functor Action V G ⥤ V.

Equations
Instances For

    F : C ⥤ Action V G preserves limits of some shape J if it does after postcomposing with the forgetful functor Action V G ⥤ V.

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

      F : C ⥤ Action V G preserves limits of some size if it does after postcomposing with the forgetful functor Action V G ⥤ V.

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

        F : C ⥤ Action V G preserves the colimit of some K : J ⥤ C if if it does after postcomposing with the forgetful functor Action V G ⥤ V.

        Equations
        Instances For

          F : C ⥤ Action V G preserves colimits of some shape J if it does after postcomposing with the forgetful functor Action V G ⥤ V.

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

            F : C ⥤ Action V G preserves colimits of some size if it does after postcomposing with the forgetful functor Action V G ⥤ V.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • Action.instPreservesLimitsOfShapeForgetOfHasLimitsOfShape = inferInstance
              Equations
              • Action.instPreservesColimitsOfShapeForgetOfHasColimitsOfShape = inferInstance
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              Equations
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              Equations
              Equations
              • Action.instZeroHom = { zero := { hom := 0, comm := } }
              Equations
              • =
              instance Action.instAddHom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {X : Action V G} {Y : Action V G} :
              Add (X Y)
              Equations
              • Action.instAddHom = { add := fun (f g : X Y) => { hom := f.hom + g.hom, comm := } }
              instance Action.instNegHom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {X : Action V G} {Y : Action V G} :
              Neg (X Y)
              Equations
              • Action.instNegHom = { neg := fun (f : X Y) => { hom := -f.hom, comm := } }
              Equations
              • Action.instPreadditive = { homGroup := fun (X Y : Action V G) => AddCommGroup.mk , add_comp := , comp_add := }
              Equations
              • =
              @[simp]
              theorem Action.neg_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {X : Action V G} {Y : Action V G} (f : X Y) :
              (-f).hom = -f.hom
              @[simp]
              theorem Action.add_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {X : Action V G} {Y : Action V G} (f : X Y) (g : X Y) :
              (f + g).hom = f.hom + g.hom
              @[simp]
              theorem Action.sum_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {X : Action V G} {Y : Action V G} {ι : Type u_1} (f : ι(X Y)) (s : Finset ι) :
              (s.sum f).hom = is, (f i).hom
              Equations
              • Action.instLinear = { homModule := fun (X Y : Action V G) => Module.mk , smul_comp := , comp_smul := }
              @[simp]
              theorem Action.smul_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R V] {X : Action V G} {Y : Action V G} (r : R) (f : X Y) :
              (r f).hom = r f.hom
              instance Action.res_additive {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {H : MonCat} (f : G H) :
              (Action.res V f).Additive
              Equations
              • =

              Auxiliary construction for the Abelian (Action V G) instance.

              Equations
              Instances For
                Equations
                Equations
                • =