Corestriction #
If S is a finite index subgroup of G and M is a G-module
then there's a corestriction map H^n(S,M) → H^n(G,M), defined
by averaging on H^0 and then by dimension shifting for
general H^n.
Remarks #
Cassels-Froehlich define cores on homology for an arbitrary
morphism S → G and then if G is finite they
extend it to Tate cohomology by dimension shifting.
It agrees with our definition on H^0-hat so presumably
agrees with our definition in general for G finite.
Arguably this filename has too large a number.
TODO #
cores o res = multiplication by index
theorem
groupCohomology.cores_aux₁
{R : Type}
[CommRing R]
{G : Type}
[Group G]
{S : Subgroup G}
{V : Type}
[AddCommMonoid V]
[Module R V]
(ρ : Representation R G V)
(v : V)
(hv : ∀ s ∈ S, (ρ s) v = v)
(g₁ g₂ : G)
(h : ↑g₁ = ↑g₂)
:
theorem
groupCohomology.cores_aux₂
{R : Type}
[CommRing R]
{G : Type}
[Group G]
{S : Subgroup G}
{X V : Type}
[Fintype X]
[AddCommGroup V]
[Module R V]
{s₁ s₂ : X → G}
(ρ : Representation R G V)
(v : V)
(hv : ∀ s ∈ S, (ρ s) v = v)
(hs₁ : Function.Bijective fun (x : X) => ↑(s₁ x))
(hs₂ : Function.Bijective fun (x : X) => ↑(s₂ x))
:
def
Rep.cores₀_obj
{R : Type}
[CommRing R]
{G : Type}
[Group G]
{S : Subgroup G}
[S.FiniteIndex]
(V : Rep R G)
:
The H^0 corestriction map for S ⊆ G a finite index subgroup, as an R-linear
map on invariants.
Equations
Instances For
@[simp]
theorem
Rep.cores₀_obj_apply_coe
{R : Type}
[CommRing R]
{G : Type}
[Group G]
{S : Subgroup G}
[S.FiniteIndex]
(V : Rep R G)
(x : ↥(V ↓ S.subtype).ρ.invariants)
:
@[simp]
theorem
groupCohomology.cores₀_app
{R : Type}
[CommRing R]
{G : Type}
[Group G]
{S : Subgroup G}
[S.FiniteIndex]
(M : Rep R G)
:
cores₀.app M = CategoryTheory.CategoryStruct.comp (H0Iso (M ↓ S.subtype)).hom
(CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom M.cores₀_obj) (H0Iso M).inv)
theorem
groupCohomology.commSq_cores₁
{R : Type}
[CommRing R]
{G : Type}
[Group G]
{S : Subgroup G}
[S.FiniteIndex]
(M : Rep R G)
:
CategoryTheory.CategoryStruct.comp (δ ⋯ 0 1 ⋯) (cores₁_obj M) = CategoryTheory.CategoryStruct.comp (cores₀.app (Rep.dimensionShift.upSES M).X₃) (δ ⋯ 0 1 ⋯)
theorem
groupCohomology.commSq_cores₁_assoc
{R : Type}
[CommRing R]
{G : Type}
[Group G]
{S : Subgroup G}
[S.FiniteIndex]
(M : Rep R G)
{Z : ModuleCat R}
(h : (functor R G 1).obj M ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (δ ⋯ 0 1 ⋯) (CategoryTheory.CategoryStruct.comp (cores₁_obj M) h) = CategoryTheory.CategoryStruct.comp (cores₀.app (Rep.dimensionShift.upSES M).X₃)
(CategoryTheory.CategoryStruct.comp (δ ⋯ 0 1 ⋯) h)
theorem
groupCohomology.cores₁_naturality
{R : Type}
[CommRing R]
{G : Type}
[Group G]
{S : Subgroup G}
[S.FiniteIndex]
(X Y : Rep R G)
(f : X ⟶ Y)
:
CategoryTheory.CategoryStruct.comp (((Rep.res S.subtype).comp (functor R (↥S) 1)).map f) (cores₁_obj Y) = CategoryTheory.CategoryStruct.comp (cores₁_obj X) ((functor R G 1).map f)
theorem
groupCohomology.cores_succ_naturality
{R : Type}
[CommRing R]
{G : Type}
[Group G]
{S : Subgroup G}
[S.FiniteIndex]
(n : ℕ)
(X Y : Rep R G)
(f : X ⟶ Y)
:
theorem
groupCohomology.map_H0Iso_hom_f_apply'
{k G H : Type u}
[CommRing k]
[Group G]
[Group H]
{A : Rep k H}
{B : Rep k G}
(f : G →* H)
(φ : A ↓ f ⟶ B)
(x : ↑(groupCohomology A 0))
:
↑((ModuleCat.Hom.hom (H0Iso B).hom) ((ModuleCat.Hom.hom (map f φ 0)) x)) = (ModuleCat.Hom.hom φ.hom) ↑((ModuleCat.Hom.hom (H0Iso A).hom) x)
theorem
groupCohomology.cores_res₀
{R : Type}
[CommRing R]
{G : Type}
[Group G]
{S : Subgroup G}
[S.FiniteIndex]
:
CategoryTheory.CategoryStruct.comp (rest S.subtype 0) cores₀ = S.index • CategoryTheory.NatTrans.id (functor R G 0)
rest cores Hⁿ(G, up M) ---> Hⁿ(S, upM ↓ S.subtype) ---> Hⁿ(G, up M) | | | δ | δ v rest cores v Hⁿ⁺¹(G, M) ---> Hⁿ⁺¹(S, M ↓ S.subtype) ---> Hⁿ⁺¹(G, M)
theorem
groupCohomology.commSqₙ
{R : Type}
[CommRing R]
{G : Type}
[Group G]
{S : Subgroup G}
[S.FiniteIndex]
(n : ℕ)
(M : Rep R G)
:
CategoryTheory.CategoryStruct.comp
((CategoryTheory.CategoryStruct.comp (rest S.subtype n) (coresNatTrans R S n)).app (Rep.dimensionShift.up.obj M))
(δ ⋯ n (n + 1) ⋯) = CategoryTheory.CategoryStruct.comp (δ ⋯ n (n + 1) ⋯)
((CategoryTheory.CategoryStruct.comp (rest S.subtype (n + 1)) (coresNatTrans R S (n + 1))).app M)
theorem
groupCohomology.cores_res
{R : Type}
[CommRing R]
{G : Type}
[Group G]
{S : Subgroup G}
[S.FiniteIndex]
(n : ℕ)
:
CategoryTheory.CategoryStruct.comp (rest S.subtype n) (coresNatTrans R S n) = S.index • CategoryTheory.NatTrans.id (functor R G n)
theorem
groupCohomology.injects_to_sylowCoh
{R : Type}
[CommRing R]
{G : Type}
[Group G]
{n : ℕ}
[NeZero n]
[Finite G]
(M : Rep R G)
(p : ℕ)
[Fact (Nat.Prime p)]
(P : Sylow p G)
:
Function.Injective
⇑(ModuleCat.Hom.hom (map (↑P).subtype (CategoryTheory.CategoryStruct.id (M ↓ (↑P).subtype)) n) ∘ₗ ↑(Module.IsTorsionBy.coprime_decompose ⋯ ⋯ ⋯).symm ∘ₗ LinearMap.inl R ↥(Submodule.torsionBy R ↑(groupCohomology M n) ↑(Nat.card ↥↑P))
↥(Submodule.torsionBy R ↑(groupCohomology M n) ↑(↑P).index))