Coinvariants.lean

1 import PaperXII.CoinvariantTensorComparison
2 import PaperXII.RightAugmentation
3 
4 set_option autoImplicit false
5 
6 /-! Paper XII, Theorem 5.4 and Corollary 11.2.
7 The commutative case uses Mathlib's tensor product in the printed order.
8 For arbitrary groups the right-module convention uses the full balanced tensor
9 with its proved universal property. No restriction on the coefficient prime. -/
10 namespace PaperXII.Coinvariants
11 
12 open scoped MonoidAlgebra TensorProduct
13 open AuxiliaryGroupAlgebra
14 
15 variable {R G M ι : Type*} [CommRing R] [AddCommGroup M] [Fintype ι]
16 
17 /-- Theorem 5.4, with both actual module isomorphisms in the displayed order. -/
18 theorem free_recovery [CommGroup G] [Module R M] [Module R[G] M]
19     [IsScalarTower R R[G] M] (b : Module.Basis ι R[G] M) :
20     let ε := augmentation (R := R) (G := G)
21     letI : Algebra R[G] R := ε.toRingHom.toAlgebra
22     Nonempty ((M ⧸ AugmentationCoinvariants.augmentationSMul (M := M) ε) ≃ₗ[R] (M ⊗[R[G]] R)) ∧
23     Nonempty ((M ⊗[R[G]] R) ≃ₗ[R] (ι → R)) := by
24   let ε := augmentation (R := R) (G := G)
25   let : Algebra R[G] R := ε.toRingHom.toAlgebra
26   let : IsScalarTower R R[G] R := IsScalarTower.of_algebraMap_eq' (by
27     ext r
28     exact (ε.commutes r).symm)
29   let c := (TensorProduct.comm R[G] M R).restrictScalars R
30   let q := Submodule.quotEquivOfEq _ _
31     (AugmentationCoinvariants.relations_eq_augmentationSMul (M := M) ε).symm
32   refine ⟨⟨q.trans ((BalancedAugmentation.tensorEquivCoinvariants ε).symm.trans
33     ((CoinvariantTensorComparison.ordinaryEquiv ε).trans c.symm))⟩, ?_⟩
34   exact ⟨c.trans (CoinvariantTensorComparison.ordinaryFreeEquiv ε b)⟩
35 
36 /-- Corollary 11.2 for arbitrary groups and coefficient rings, hence for finite
37 two-groups and dyadic coefficient rings. A right basis is used for M ⊗[R[G]] R. -/
38 theorem dyadic_free_recovery [Group G] [Module R M] [Module (R[G])ᵐᵒᵖ M]
39     [IsScalarTower R (R[G])ᵐᵒᵖ M] (b : Module.Basis ι (R[G])ᵐᵒᵖ M) :
40     let ε := augmentation (R := R) (G := G)
41     Nonempty (RightAugmentation.Tensor (M := M) ε ≃ₗ[R]
42       (M ⧸ RightAugmentation.augmentationSMul (M := M) ε)) ∧
43     Nonempty (Module.Basis ι R (RightAugmentation.Tensor (M := M) ε)) := by
44   exact ⟨⟨RightAugmentation.tensorEquivQuotient _⟩,
45     ⟨RightAugmentation.recoveredBasis _ b⟩⟩
46 
47 end PaperXII.Coinvariants

Back to source controls