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 (X.V →₀ k)

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.

@[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 = Finsupp.lmapDomain k k (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) fun₀ | x => 1) = fun₀ | 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.

@[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) fun₀ | x => r) = fun₀ | f.hom x => r

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 = Finsupp.lmapDomain k k f.hom

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.MonoidalCategoryStruct.tensorObj X Y).ρ g xy = (X.ρ g xy.1, 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.

@[simp]

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

theorem Representation.LinearizeMonoidal.ε_one {k : Type u} {G : Type v} [Monoid G] [Semiring k] : (ε k G) 1 = fun₀ | 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.

@[simp]

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

theorem Representation.LinearizeMonoidal.η_single {k : Type u} {G : Type v} [Monoid G] [Semiring k] (x : PUnit.{u + 1}) : ((η k G) fun₀ | 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.

@[simp]

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

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) ((fun₀ | x => r) ⊗ₜ[k] fun₀ | y => s) = fun₀ | (x, y) => r * s

theorem Representation.LinearizeMonoidal.μ_apply_apply {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (l1 : X.V →₀ k) (l2 : Y.V →₀ k) (xy : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).V) : ((μ X Y) (l1 ⊗ₜ[k] l2)) xy = l1 xy.1 * l2 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.

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) fun₀ | xy => 1) = (fun₀ | xy.1 => 1) ⊗ₜ[k] fun₀ | 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 (X →₀ k))

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

theorem Representation.linearizeTrivialIso_apply {k : Type u} {G : Type v} [Monoid G] [Semiring k] {X : Type w} (f : (Action.trivial G X).V →₀ k) : (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 : X →₀ k) : (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.

theorem Representation.linearizeOfMulActionIso_apply {k : Type u} {G : Type v} [Monoid G] [Semiring k] {H : Type w} [MulAction G H] (f : H →₀ k) : (linearizeOfMulActionIso k G H) f = f

theorem Representation.linearizeOfMulActionIso_symm_apply {k : Type u} {G : Type v} [Monoid G] [Semiring k] {H : Type w} [MulAction G H] (f : H →₀ k) : (linearizeOfMulActionIso k G H).symm f = f

@[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.