Main Purpose

This file is the preliminary for the linearize functor from Action (Type w) G to Rep k G, constructing the functor from the Representation would reduce the amount of DefEq abuses that we currently are doing in the Rep file.

TODO (Edison) : Refactor Rep to be a concrete category of Representation and reconstruct the current linearize functor using this file.

noncomputable def Representation.linearize (k : Type u) (G : Type v) [Monoid G] [Semiring k] (X : Action (Type w) G) : Representation k G (MonoidAlgebra k X.V)

Every Set X that has a G-action on it can be made into a G-rep by using X →₀ k as the base module and G-action on it is induced by the G-action on X.

Equations

• Representation.linearize k G X = { toFun := fun (g : G) => MonoidAlgebra.mapDomainLinearMap k k ⇑(CategoryTheory.ConcreteCategory.hom (X.ρ g)), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Representation.linearize_apply (k : Type u) (G : Type v) [Monoid G] [Semiring k] (X : Action (Type w) G) (g : G) : (linearize k G X) g = MonoidAlgebra.mapDomainLinearMap k k ⇑(CategoryTheory.ConcreteCategory.hom (X.ρ g))

theorem Representation.linearize_single {k : Type u} {G : Type v} [Monoid G] [Semiring k] {X : Action (Type w) G} (g : G) (x : X.V) : ((linearize k G X) g) (MonoidAlgebra.single x 1) = MonoidAlgebra.single ((CategoryTheory.ConcreteCategory.hom (X.ρ g)) x) 1

noncomputable def Representation.linearizeMap {k : Type u} {G : Type v} [Monoid G] [Semiring k] {X Y : Action (Type w) G} (f : X ⟶ Y) : (linearize k G X).IntertwiningMap (linearize k G Y)

Every morphism between G-sets could be made into an intertwining map between Representations by the linear map induced on the indexing sets.

Equations

• Representation.linearizeMap f = { toLinearMap := MonoidAlgebra.mapDomainLinearMap k k ⇑(CategoryTheory.ConcreteCategory.hom f.hom), isIntertwining' := ⋯ }

@[simp]

theorem Representation.linearizeMap_toLinearMap {k : Type u} {G : Type v} [Monoid G] [Semiring k] {X Y : Action (Type w) G} (f : X ⟶ Y) : (linearizeMap f).toLinearMap = MonoidAlgebra.mapDomainLinearMap k k ⇑(CategoryTheory.ConcreteCategory.hom f.hom)

@[simp]

theorem Representation.linearizeMap_single {k : Type u} {G : Type v} [Monoid G] [Semiring k] {X Y : Action (Type w) G} (f : X ⟶ Y) (x : X.V) (r : k) : (linearizeMap f) (MonoidAlgebra.single x r) = MonoidAlgebra.single ((CategoryTheory.ConcreteCategory.hom f.hom) x) r

theorem Action.tensor_ρ_apply {G : Type v} [Monoid G] {X Y : Action (Type w) G} (g : G) (xy : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).V) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).ρ g)) xy = ((CategoryTheory.ConcreteCategory.hom (X.ρ g)) xy.1, (CategoryTheory.ConcreteCategory.hom (Y.ρ g)) xy.2)

noncomputable def Representation.LinearizeMonoidal.ε (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (trivial k G k).IntertwiningMap (linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type w) G)))

The counit of the linearize functor.

Equations

• Representation.LinearizeMonoidal.ε k G = { toLinearMap := ↑(MonoidAlgebra.uniqueLinearEquiv k PUnit.{?u.3 + 1}).symm, isIntertwining' := ⋯ }

@[simp]

theorem Representation.LinearizeMonoidal.ε_toLinearMap (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (ε k G).toLinearMap = ↑(MonoidAlgebra.uniqueLinearEquiv k PUnit.{w + 1}).symm

theorem Representation.LinearizeMonoidal.ε_one {k : Type u} {G : Type v} [Monoid G] [Semiring k] : (ε k G) 1 = MonoidAlgebra.single PUnit.unit 1

noncomputable def Representation.LinearizeMonoidal.η (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G))).IntertwiningMap (trivial k G k)

The unit of the linearize functor.

Equations

• Representation.LinearizeMonoidal.η k G = { toLinearMap := ↑(MonoidAlgebra.uniqueLinearEquiv k PUnit.{?u.2 + 1}), isIntertwining' := ⋯ }

@[simp]

theorem Representation.LinearizeMonoidal.η_toLinearMap (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (η k G).toLinearMap = ↑(MonoidAlgebra.uniqueLinearEquiv k PUnit.{u + 1})

theorem Representation.LinearizeMonoidal.η_single {k : Type u} {G : Type v} [Monoid G] [Semiring k] (x : PUnit.{u + 1}) : (η k G) (MonoidAlgebra.single x 1) = 1

theorem Representation.LinearizeMonoidal.ε_η (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (ε k G).comp (η k G) = IntertwiningMap.id (linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G)))

theorem Representation.LinearizeMonoidal.η_ε (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (η k G).comp (ε k G) = IntertwiningMap.id (trivial k G k)

noncomputable def Representation.LinearizeMonoidal.μ {G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : ((linearize k G X).tprod (linearize k G Y)).IntertwiningMap (linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))

The tensor (multiplication) of the linearize functor.

Equations

• Representation.LinearizeMonoidal.μ X Y = { toLinearMap := ↑(MonoidAlgebra.tensorEquiv k), isIntertwining' := ⋯ }

@[simp]

theorem Representation.LinearizeMonoidal.μ_toLinearMap {G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : (μ X Y).toLinearMap = ↑(MonoidAlgebra.tensorEquiv k)

theorem Representation.LinearizeMonoidal.μ_apply_single_single {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (x : X.V) (y : Y.V) (r s : k) : (μ X Y) (MonoidAlgebra.single x r ⊗ₜ[k] MonoidAlgebra.single y s) = MonoidAlgebra.single (x, y) (r * s)

theorem Representation.LinearizeMonoidal.coeff_μ_tmul {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (l1 : MonoidAlgebra k X.V) (l2 : MonoidAlgebra k Y.V) (xy : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).V) : ((μ X Y) (l1 ⊗ₜ[k] l2)).coeff xy = l1.coeff xy.1 * l2.coeff xy.2

theorem Representation.LinearizeMonoidal.μ_comp_rTensor {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (f : X ⟶ Y) (Z : Action (Type w) G) : (μ Y Z).comp (IntertwiningMap.rTensor (linearize k G Z) (linearizeMap f)) = (linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)).comp (μ X Z)

theorem Representation.LinearizeMonoidal.μ_comp_lTensor {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (f : X ⟶ Y) (Z : Action (Type w) G) : (μ Z Y).comp (IntertwiningMap.lTensor (linearize k G Z) (linearizeMap f)) = (linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)).comp (μ Z X)

theorem Representation.LinearizeMonoidal.μ_comp_assoc {G : Type v} [Monoid G] (X Y Z : Action (Type w) G) {k : Type u} [CommSemiring k] : ((linearizeMap (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom).comp (μ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)).comp (IntertwiningMap.rTensor (linearize k G Z) (μ X Y)) = ((μ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).comp (IntertwiningMap.lTensor (linearize k G X) (μ Y Z))).comp ↑(TensorProduct.assoc (linearize k G X) (linearize k G Y) (linearize k G Z))

theorem Representation.LinearizeMonoidal.μ_leftUnitor {G : Type v} [Monoid G] (X : Action (Type w) G) {k : Type u} [CommSemiring k] : ↑(TensorProduct.lid k (linearize k G X)) = ((linearizeMap (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom).comp (μ (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type w) G)) X)).comp (IntertwiningMap.rTensor (linearize k G X) (ε k G))

theorem Representation.LinearizeMonoidal.μ_rightUnitor {G : Type v} [Monoid G] (X : Action (Type w) G) {k : Type u} [CommSemiring k] : ↑(TensorProduct.rid k (linearize k G X)) = ((linearizeMap (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom).comp (μ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type w) G)))).comp (IntertwiningMap.lTensor (linearize k G X) (ε k G))

noncomputable def Representation.LinearizeMonoidal.δ {G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : (linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).IntertwiningMap ((linearize k G X).tprod (linearize k G Y))

The comultiplication of the linearize functor.

Equations

• Representation.LinearizeMonoidal.δ X Y = { toLinearMap := ↑(MonoidAlgebra.tensorEquiv k).symm, isIntertwining' := ⋯ }

theorem Representation.LinearizeMonoidal.δ_apply_single {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (xy : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).V) : (δ X Y) (MonoidAlgebra.single xy 1) = MonoidAlgebra.single xy.1 1 ⊗ₜ[k] MonoidAlgebra.single xy.2 1

theorem Representation.LinearizeMonoidal.rTensor_comp_δ {G : Type v} [Monoid G] {X Y : Action (Type w) G} (Z : Action (Type w) G) {k : Type u} [CommSemiring k] (f : X ⟶ Y) : (IntertwiningMap.rTensor (linearize k G Z) (linearizeMap f)).comp (δ X Z) = (δ Y Z).comp (linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z))

theorem Representation.LinearizeMonoidal.lTensor_comp_δ {G : Type v} [Monoid G] {X Y : Action (Type w) G} (Z : Action (Type w) G) {k : Type u} [CommSemiring k] (f : X ⟶ Y) : (IntertwiningMap.lTensor (linearize k G Z) (linearizeMap f)).comp (δ Z X) = (δ Z Y).comp (linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f))

theorem Representation.LinearizeMonoidal.assoc_comp_δ {G : Type v} [Monoid G] (X Y Z : Action (Type w) G) {k : Type u} [CommSemiring k] : ((↑(TensorProduct.assoc (linearize k G X) (linearize k G Y) (linearize k G Z))).comp (IntertwiningMap.rTensor (linearize k G Z) (δ X Y))).comp (δ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) = ((IntertwiningMap.lTensor (linearize k G X) (δ Y Z)).comp (δ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))).comp (linearizeMap (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)

theorem Representation.LinearizeMonoidal.leftUnitor_δ {G : Type v} [Monoid G] {k : Type u} [CommSemiring k] (X : Action (Type u) G) : ↑(TensorProduct.lid k (linearize k G X)).symm = ((IntertwiningMap.rTensor (linearize k G X) (η k G)).comp (δ (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G)) X)).comp (linearizeMap (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv)

theorem Representation.LinearizeMonoidal.rightUnitor_δ {G : Type v} [Monoid G] {k : Type u} [CommSemiring k] (X : Action (Type u) G) : ↑(TensorProduct.rid k (linearize k G X)).symm = ((IntertwiningMap.lTensor (linearize k G X) (η k G)).comp (δ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G)))).comp (linearizeMap (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv)

theorem Representation.LinearizeMonoidal.μ_δ {G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : (μ X Y).comp (δ X Y) = IntertwiningMap.id (linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))

theorem Representation.LinearizeMonoidal.δ_μ {G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : (δ X Y).comp (μ X Y) = IntertwiningMap.id ((linearize k G X).tprod (linearize k G Y))

theorem Representation.linearizeTrivial_def {k : Type u} {G : Type v} [Monoid G] [Semiring k] (X : Type w) (g : G) : (linearize k G (Action.trivial G X)) g = LinearMap.id

noncomputable def Representation.linearizeTrivialIso (k : Type u) (G : Type v) [Monoid G] [Semiring k] (X : Type w) : (linearize k G (Action.trivial G X)).Equiv (trivial k G (MonoidAlgebra k X))

This a type-changing equivalence (which requires a non-trivial proof that LinearEquiv.refl _ _ is G-equivariant) to avoid abusing defeq.

Equations

• Representation.linearizeTrivialIso k G X = Representation.Equiv.mk (LinearEquiv.refl k (MonoidAlgebra k (Action.trivial G X).V)) ⋯

theorem Representation.linearizeTrivialIso_apply {k : Type u} {G : Type v} [Monoid G] [Semiring k] {X : Type w} (f : MonoidAlgebra k (Action.trivial G X).V) : (linearizeTrivialIso k G X) f = f

theorem Representation.linearizeTrivialIso_symm_apply {k : Type u} {G : Type v} [Monoid G] [Semiring k] {X : Type w} (f : MonoidAlgebra k X) : (linearizeTrivialIso k G X).symm f = f

noncomputable def Representation.linearizeOfMulActionIso (k : Type u) (G : Type v) [Monoid G] [Semiring k] (H : Type w) [MulAction G H] : (linearize k G (Action.ofMulAction G H)).Equiv (ofMulAction k G H)

This a type-changing equivalence to avoid abusing defeq.

Equations

• Representation.linearizeOfMulActionIso k G H = Representation.Equiv.mk (LinearEquiv.refl k (MonoidAlgebra k (Action.ofMulAction G H).V)) ⋯

@[reducible, inline]

noncomputable abbrev Representation.linearizeDiagonalEquiv (k : Type u) (G : Type v) [Monoid G] [Semiring k] (n : ℕ) : (linearize k G (Action.diagonal G n)).Equiv (diagonal k G n)

This a type-changing equivalence to avoid abusing defeq.

Equations

• Representation.linearizeDiagonalEquiv k G n = Representation.linearizeOfMulActionIso k G (Fin n → G)