Rep.to_Module_monoidAlgebra_map_aux
theorem Rep.to_Module_monoidAlgebra_map_aux :
∀ {k : Type u_1} {G : Type u_2} [inst : CommRing k] [inst_1 : Monoid G] (V : Type u_3) (W : Type u_4)
[inst_2 : AddCommGroup V] [inst_3 : AddCommGroup W] [inst_4 : Module k V] [inst_5 : Module k W]
(ρ : G →* V →ₗ[k] V) (σ : G →* W →ₗ[k] W) (f : V →ₗ[k] W),
(∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f) →
∀ (r : MonoidAlgebra k G) (x : V),
f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) r) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) r) (f x)
This theorem, `Rep.to_Module_monoidAlgebra_map_aux`, establishes a property of the interaction between monoid algebras and linear transformations. Given a commutative ring `k`, a monoid `G`, additive commutative groups `V` and `W`, and `V` and `W` being modules over `k`. Also given are two monoid homomorphisms `ρ` and `σ` from `G` to the endomorphisms of `V` and `W` respectively, and a linear map `f` from `V` to `W`. If for all `g` in `G`, the composition of `f` with `ρ g` equals the composition of `σ g` with `f`, then for all `r` in the monoid algebra of `k` and `G`, and all `x` in `V`, applying `f` to the result of applying the lift of `ρ` to `r` and then applying that to `x` equals applying the lift of `σ` to `r`, applying that to `f x`. In simpler terms, this theorem states that under the given conditions, applying `f` after a certain operation in the monoid algebra yields the same result as a similar operation in the monoid algebra applied after `f`.
More concisely: Given commutative ring `k`, monoids `G`, modules `V` and `W` over `k`, monoid homomorphisms `ρ` and `σ` from `G` to the endomorphisms of `V` and `W` respectively, and a linear map `f` from `V` to `W` such that `f ∘ ρ(g) = σ(g) ∘ f` for all `g` in `G`, then for all `r` in the monoid algebra of `k` and `G`, and all `x` in `V`, `f(ρ(r)(x)) = σ(r)(f(x))`.
|
Rep.homEquiv_apply_hom
theorem Rep.homEquiv_apply_hom :
∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep k G}
(f : CategoryTheory.MonoidalCategory.tensorObj A B ⟶ C),
((A.homEquiv B C) f).hom = (TensorProduct.curry f.hom).flip
This theorem, named `Rep.homEquiv_apply_hom`, states that for any commutative ring `k`, any group `G`, and any three `k`-linear representations (`Rep k G`) `A`, `B`, and `C` of `G`, and any morphism `f` from the monoidal tensor object of `A` and `B` to `C`, the homomorphism corresponding to `f` under the equivalence `A.homEquiv B C` is the same as the flip of the curried version of the homomorphism `f`. In simpler terms, it connects the operations of tensor products and homomorphisms in the category of `k`-linear representations of a group `G`, and expresses a certain symmetry property of these operations.
More concisely: For any commutative ring `k`, group `G`, and `k`-linear representations `A`, `B`, `C` of `G`, and morphism `f : A ⊗ B → C`, the homomorphism `(A.homEquiv B C).toFun . f` is equal to the flip of `f.map (A.homEquiv B C)`.
|
Rep.homEquiv_symm_apply_hom
theorem Rep.homEquiv_symm_apply_hom :
∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep k G} (f : B ⟶ A.ihom.obj C),
((A.homEquiv B C).symm f).hom =
(TensorProduct.uncurry k (CoeSort.coe A) (CoeSort.coe B) (CoeSort.coe C)) (LinearMap.flip f.hom)
The theorem `Rep.homEquiv_symm_apply_hom` states that for any commutative ring `k`, group `G`, and k-linear representations `A`, `B`, and `C` of the group `G`, and for a morphism `f` from `B` to the hom object of `A` and `C`, the hom of the inverse of the homomorphism equivalence of `A`, `B`, `C` applied to `f` equals the uncurry function of the tensor product of `k`, `A`, `B`, `C` applied to the flipped version of the hom of `f`.
In other words, this theorem is about the relationship between the inverse of a homomorphism equivalence and the uncurry function of the tensor product in the context of k-linear representations of a group. It is essentially a property of the structure of a category of representations, specifically how the morphisms interact with the tensor product structure.
More concisely: For any commutative ring `k`, group `G`, and k-linear representations `A`, `B`, `C` of `G`, and a morphism `f` from `B` to `A ⟶ C`, the inverse of the homomorphism equivalence of `A`, `B`, `C` applied to `f` equals the uncurry of `k ⊗ A ⊗ B ⊗ C ⏜ (flip (f ∘_ C))`.
|
Rep.of_ρ_apply
theorem Rep.of_ρ_apply :
∀ {k G : Type u} [inst : CommRing k] [inst_1 : Monoid G] {V : Type u} [inst_2 : AddCommGroup V]
[inst_3 : Module k V] (ρ : Representation k G V) (g : ↑(MonCat.of G)), (Rep.of ρ).ρ g = ρ g
The theorem `Rep.of_ρ_apply` states that for any commutative ring `k`, any monoid `G`, and any type `V` that is an additive commutative group and a `k`-module, if `ρ` is a representation of `G` on the `k`-module `V`, then applying `ρ` to an element `g` of the monoid `G` (where `g` is seen as an element of the corresponding object in the category of monoids) gives the same result as applying the representation obtained from `ρ` by the `Rep.of` function to `g`. Essentially, this theorem allows us to apply lemmas about the underlying representation `ρ` to elements of the monoid `G`, even when viewed as elements of the monoidal category.
More concisely: For any commutative ring `k`, monoid `G`, and additive commutative `k`-module `V` with a representation `ρ`, applying `ρ` to an element `g` in `G` is equivalent to applying the representation `Rep.of ρ` to `g` in the monoidal category.
|