Rep.diagonalHomEquiv_apply
theorem Rep.diagonalHomEquiv_apply :
∀ {k G : Type u} [inst : CommRing k] {n : ℕ} [inst_1 : Group G] {A : Rep k G}
(f : Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) (x : Fin n → G),
(Rep.diagonalHomEquiv n A) f x = f.hom fun₀ | Fin.partialProd x => 1
This theorem, `Rep.diagonalHomEquiv_apply`, states that for any `k`-linear `G`-representation `A`, there exists a `k`-linear isomorphism between the set of representation morphisms `Hom(k[Gⁿ⁺¹], A)` and `Fun(Gⁿ, A)`, which is denoted as `diagonalHomEquiv`. More specifically, the isomorphism maps a morphism of representations `f : k[Gⁿ⁺¹] ⟶ A` to the function `(g₁, ..., gₙ) ↦ f(1, g₁, g₁g₂, ..., g₁g₂...gₙ)`. Here, `k` is a commutative ring, `G` is a group, `n` is a natural number, and `A` is a `k`-linear `G`-representation. The `f.hom fun₀ | Fin.partialProd x => 1` term in the theorem is the result of applying the `f` morphism to the partial product of `x`.
More concisely: For any `k`-linear `G`-representation `A`, there exists a `k`-linear isomorphism between the set of representation morphisms `Hom(k[Gⁿ⁺¹], A)` and `Fun(Gⁿ, A)`, which maps a morphism `f` to the function `(g₁, ..., gₙ) ↦ f(1, g₁, g₁g₂, ..., g₁g₂...gₙ)`.
|
groupCohomology.resolution.d_eq
theorem groupCohomology.resolution.d_eq :
∀ (k G : Type u) [inst : CommRing k] [inst_1 : Monoid G] (n : ℕ),
((groupCohomology.resolution k G).d (n + 1) n).hom = groupCohomology.resolution.d k G (n + 1)
This theorem provides a simplified expression for the differential in the standard resolution of `k` as a `G`-representation. Specifically, it states that for any commutative ring `k`, monoid `G`, and natural number `n`, the differential operator `d` at the `n+1`-th spot in the chain complex that represents the standard resolution of `k` as a `G`-representation is equal to the `n+1`-th differential in the group cohomology resolution. The differential sends a tuple `(g₀, ..., gₙ₊₁)` to the sum of `(-1)ⁱ` times the tuple `(g₀, ..., ĝᵢ, ..., gₙ₊₁)`, where the hat indicates that the `i`-th term is omitted.
More concisely: The differential at the `(n+1)`-th position in the standard resolution of a commutative ring `k` as a `G`-representation equals the `(n+1)`-th differential in the group cohomology resolution.
|
Rep.diagonalHomEquiv_symm_partialProd_succ
theorem Rep.diagonalHomEquiv_symm_partialProd_succ :
∀ {k G : Type u} [inst : CommRing k] {n : ℕ} [inst_1 : Group G] {A : Rep k G} (f : (Fin n → G) → CoeSort.coe A)
(g : Fin (n + 1) → G) (a : Fin (n + 1)),
(((Rep.diagonalHomEquiv n A).symm f).hom fun₀ | Fin.partialProd g ∘ a.succ.succAbove => 1) =
f (a.contractNth (fun x x_1 => x * x_1) g)
This theorem, `Rep.diagonalHomEquiv_symm_partialProd_succ`, serves as an auxiliary lemma for defining group cohomology. It asserts that for any commutative ring `k`, group `G`, representation `A` of `G` over `k`, function `f` from mappings from `Fin n` to `G` to the coercing type of `A`, function `g` from `Fin (n + 1)` to `G`, and element `a` of `Fin (n + 1)`, the result of applying the inverse of the diagonal homomorphism equivalence `Rep.diagonalHomEquiv` to `f`, and then the homomorphism function to the composition of `Fin.partialProd g` and the function `a.succ.succAbove` is equal to the result of applying `f` to the result of contracting `a` in the product of function `g`. This theorem is used to demonstrate that the isomorphism `diagonalHomEquiv` commutes with the differentials in two complexes which are used to compute group cohomology.
More concisely: For any commutative ring `k`, group `G`, representation `A` of `G` over `k`, functions `f` and `g`, and element `a`, the inverse of the diagonal homomorphism equivalence applied to `f` and then the homomorphism function to the composition of `g` and `a.succ.succAbove` equals `f` applied to the contraction of `a` in the product of `g`.
|
Rep.diagonalHomEquiv_symm_apply
theorem Rep.diagonalHomEquiv_symm_apply :
∀ {k G : Type u} [inst : CommRing k] {n : ℕ} [inst_1 : Group G] {A : Rep k G} (f : (Fin n → G) → CoeSort.coe A)
(x : Fin (n + 1) → G),
(((Rep.diagonalHomEquiv n A).symm f).hom fun₀ | x => 1) = (A.ρ (x 0)) (f fun i => (x i.castSucc)⁻¹ * x i.succ)
The theorem `Rep.diagonalHomEquiv_symm_apply` states that for any commutative ring `k`, natural number `n`, group `G`, and `k`-linear `G`-representation `A`, given a function `f` from the `n`-dimensional vector space over `G` to `A` (interpreted via the coercion `CoeSort.coe`), and a sequence `x` of `n + 1` elements from `G`, the inverse of the `k`-linear isomorphism `diagonalHomEquiv` (which relates the set of representation morphisms from `k[Gⁿ⁺¹]` to `A` and functions from `Gⁿ` to `A`) applied to `f` (which gives a representation morphism), when applied to the function `fun₀ | x => 1`, equals the application of the `G`-action `ρ` on `x 0`, to `f` applied to the function that maps each `i` to the product of the inverse of `x i.castSucc` and `x i.succ`. Here, `ρ` denotes the representation attached to `A`.
More concisely: For any commutative ring `k`, natural number `n`, group `G`, `k`-linear `G`-representation `A`, function `f` from the `n`-dimensional `G`-module to `A`, and sequence `x` of `n + 1` elements from `G`, the application of the inverse of `diagonalHomEquiv` on `f` to the constant function `fun⁰ | x => 1`, is equivalent to applying the `G`-action on `x 0` to `f` followed by the function that maps each `i` to the product of the inverse of `x i.castSucc` and `x i.succ`.
|
groupCohomology.resolution.forget₂ToModuleCatHomotopyEquiv_f_0_eq
theorem groupCohomology.resolution.forget₂ToModuleCatHomotopyEquiv_f_0_eq :
∀ (k G : Type u) [inst : CommRing k] [inst_1 : Monoid G],
(groupCohomology.resolution.forget₂ToModuleCatHomotopyEquiv k G).hom.f 0 =
(CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).map (groupCohomology.resolution.ε k G)
This theorem states that, for any commutative ring `k` and any monoid `G`, the homotopy equivalence of complexes of `k`-modules between the standard resolution of `k` as a trivial `G`-representation and the complex which is `k` at 0 and 0 everywhere else, acts as the mapping `∑ nᵢgᵢ ↦ ∑ nᵢ : k[G¹] → k` at the 0th index. This is expressed in terms of the forgetful functor from the category of `k`-linear `G`-representations to the category of `k`-modules.
More concisely: The standard resolution of the trivial `G`-representation of a commutative ring `k` is homotopy equivalent to the constant `k`-complex, and the corresponding map between their representational complexes is the summation homomorphism from `k[G]` to `k`.
|