CoinvariantTensorComparison.lean

1 import PaperXII.BalancedAugmentation
2 import Mathlib.LinearAlgebra.TensorProduct.Tower
3 
4 set_option autoImplicit false
5 
6 /-! Comparison with Mathlib's tensor product when the augmented algebra is
7 commutative. The noncommutative construction retains its proved universal property. -/
8 namespace PaperXII.CoinvariantTensorComparison
9 
10 open scoped TensorProduct
11 open BalancedAugmentation
12 
13 variable {R A M : Type*} [CommRing R] [CommRing A] [Algebra R A]
14   [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M]
15 
16 /-- The coefficient-bilinear map to the ordinary tensor product over A. -/
17 noncomputable def ordinaryMk (ε : A →ₐ[R] R) :
18     letI : Algebra A R := ε.toRingHom.toAlgebra
19     R →ₗ[R] M →ₗ[R] (R ⊗[A] M) := by
20   letI : Algebra A R := ε.toRingHom.toAlgebra
21   letI : IsScalarTower R A R := IsScalarTower.of_algebraMap_eq' (by
22     ext r
23     exact (ε.commutes r).symm)
24   exact (TensorProduct.mk R R M).compr₂ (TensorProduct.mapOfCompatibleSMul A R R R M)
25 
26 /-- This comparison uses the original pure tensor. -/
27 theorem ordinaryMk_apply (ε : A →ₐ[R] R) (r : R) (m : M) :
28     letI : Algebra A R := ε.toRingHom.toAlgebra
29     ordinaryMk ε r m = r ⊗ₜ[A] m := rfl
30 
31 /-- The ordinary tensor map has the augmentation balancing law. -/
32 theorem ordinaryMk_balanced (ε : A →ₐ[R] R) (r : R) (a : A) (m : M) :
33     letI : Algebra A R := ε.toRingHom.toAlgebra
34     ordinaryMk ε r (a • m) = ordinaryMk ε (r * ε a) m := by
35   let : Algebra A R := ε.toRingHom.toAlgebra
36   change r ⊗ₜ[A] (a • m) = (r * ε a) ⊗ₜ[A] m
37   rw [← TensorProduct.smul_tmul]
38   change (ε a * r) ⊗ₜ[A] m = (r * ε a) ⊗ₜ[A] m
39   rw [mul_comm]
40 
41 /-- Descend to Mathlib's tensor product. -/
42 noncomputable def toOrdinary (ε : A →ₐ[R] R) :
43     letI : Algebra A R := ε.toRingHom.toAlgebra
44     Tensor (M := M) ε →ₗ[R] (R ⊗[A] M) :=
45   lift ε (ordinaryMk ε) (ordinaryMk_balanced ε)
46 
47 /-- Build the inverse using the additive balanced universal property. -/
48 noncomputable def fromOrdinary (ε : A →ₐ[R] R) :
49     letI : Algebra A R := ε.toRingHom.toAlgebra
50     (R ⊗[A] M) →ₗ[R] Tensor (M := M) ε := by
51   letI : Algebra A R := ε.toRingHom.toAlgebra
52   let f : R →+ M →+ Tensor (M := M) ε := {
53     toFun := fun r => (tensorMk ε r).toAddMonoidHom
54     map_zero' := by ext m; simp
55     map_add' := by intro r s; ext m; simp }
56   let hf : ∀ a r m, f (a • r) m = f r (a • m) := by
57     intro a r m
58     change tensorMk ε (ε a * r) m = tensorMk ε r (a • m)
59     rw [mul_comm]
60     exact (tensorMk_balanced ε r a m).symm
61   let F := TensorProduct.liftAddHom f hf
62   exact {
63     F with
64     map_smul' := by
65       intro r x
66       change F (r • x) = r • F x
67       induction x using TensorProduct.induction_on with
68       | zero => simp
69       | add x y hx hy => simp [hx, hy, smul_add]
70       | tmul s m =>
71         rw [TensorProduct.smul_tmul']
72         change tensorMk ε (r • s) m = r • tensorMk ε s m
73         rw [map_smul, LinearMap.smul_apply] }
74 
75 /-- Both comparisons fix the pure tensors. -/
76 theorem toOrdinary_tensorMk (ε : A →ₐ[R] R) (r : R) (m : M) :
77     letI : Algebra A R := ε.toRingHom.toAlgebra
78     toOrdinary ε (tensorMk ε r m) = r ⊗ₜ[A] m := rfl
79 
80 omit [IsScalarTower R A M] in
81 /-- The inverse comparison fixes pure tensors. -/
82 theorem fromOrdinary_tmul (ε : A →ₐ[R] R) (r : R) (m : M) :
83     letI : Algebra A R := ε.toRingHom.toAlgebra
84     fromOrdinary ε (r ⊗ₜ[A] m) = tensorMk ε r m := rfl
85 
86 /-- The constructed balanced tensor is Mathlib's ordinary tensor in the commutative case. -/
87 noncomputable def ordinaryEquiv (ε : A →ₐ[R] R) :
88     letI : Algebra A R := ε.toRingHom.toAlgebra
89     Tensor (M := M) ε ≃ₗ[R] (R ⊗[A] M) := by
90   letI : Algebra A R := ε.toRingHom.toAlgebra
91   refine LinearEquiv.ofLinearMap (toOrdinary ε) (fromOrdinary ε) ?_ ?_
92   · apply TensorProduct.AlgebraTensorModule.ext
93     intro r m
94     change toOrdinary ε (fromOrdinary ε (r ⊗ₜ[A] m)) = r ⊗ₜ[A] m
95     rw [fromOrdinary_tmul, toOrdinary_tensorMk]
96   · apply BalancedAugmentation.hom_ext ε
97     intro r m
98     change fromOrdinary ε (toOrdinary ε (tensorMk ε r m)) = tensorMk ε r m
99     rw [toOrdinary_tensorMk, fromOrdinary_tmul]
100 
101 /-- The full ordinary free-module recovery, with the usual tensor product. -/
102 noncomputable def ordinaryFreeEquiv {ι : Type*} [Fintype ι]
103     (ε : A →ₐ[R] R) (b : Module.Basis ι A M) :
104     letI : Algebra A R := ε.toRingHom.toAlgebra
105     (R ⊗[A] M) ≃ₗ[R] (ι → R) :=
106   (ordinaryEquiv ε).symm.trans (freeTensorEquiv ε b)
107 
108 end PaperXII.CoinvariantTensorComparison

Back to source controls