BalancedAugmentation.lean

1 import PaperXII.AugmentationCoinvariants
2 import Mathlib.LinearAlgebra.TensorProduct.Associator
3 
4 set_option autoImplicit false
5 
6 /-! The actual balanced tensor product R ⊗[A,ε] M for a possibly
7 noncommutative augmented R-algebra A. Start with R ⊗[R] M and quotient
8 by all A-balancing relations. This fixes the left-module convention. -/
9 namespace PaperXII.BalancedAugmentation
10 
11 open scoped TensorProduct
12 open AugmentationCoinvariants
13 
14 variable {R A M : Type*} [CommRing R] [Ring A] [Algebra R A]
15   [AddCommGroup M] [Module R M] [Module A M]
16 
17 /-- All balancing relations for the right action r·a = r ε(a) on R. -/
18 def tensorRelations (ε : A →ₐ[R] R) : Submodule R (R ⊗[R] M) :=
19   Submodule.span R (Set.range fun ram : R × A × M =>
20     ram.1 ⊗ₜ[R] (ram.2.1 • ram.2.2) - (ram.1 * ε ram.2.1) ⊗ₜ[R] ram.2.2)
21 
22 /-- The balanced tensor product, defined by the full relation quotient. -/
23 abbrev Tensor (ε : A →ₐ[R] R) := (R ⊗[R] M) ⧸ tensorRelations (M := M) ε
24 
25 /-- Its canonical coefficient-bilinear tensor map. -/
26 def tensorMk (ε : A →ₐ[R] R) : R →ₗ[R] M →ₗ[R] Tensor (M := M) ε :=
27   (TensorProduct.mk R R M).compr₂ (tensorRelations ε).mkQ
28 
29 /-- The canonical tensor map satisfies every A-balancing equation. -/
30 theorem tensorMk_balanced (ε : A →ₐ[R] R) (r : R) (a : A) (m : M) :
31     tensorMk ε r (a • m) = tensorMk ε (r * ε a) m :=
32   (Submodule.Quotient.eq _).mpr (Submodule.subset_span (Set.mem_range_self (r,a,m)))
33 
34 /-- The coefficient factor is generated by one. -/
35 theorem tensorMk_scalar (ε : A →ₐ[R] R) (r : R) (m : M) :
36     tensorMk ε r m = r • tensorMk ε 1 m := by
37   have h : tensorMk ε (r • (1 : R)) m = r • tensorMk ε 1 m := by
38     rw [map_smul, LinearMap.smul_apply]
39   simpa only [smul_eq_mul, mul_one] using h
40 
41 variable {W : Type*} [AddCommGroup W] [Module R W]
42 
43 /-- Every balanced bilinear map descends to the actual tensor quotient. -/
44 def lift (ε : A →ₐ[R] R) (f : R →ₗ[R] M →ₗ[R] W)
45     (hf : ∀ r a m, f r (a • m) = f (r * ε a) m) : Tensor (M := M) ε →ₗ[R] W :=
46   (tensorRelations ε).liftQ (TensorProduct.lift f) (Submodule.span_le.mpr <| by
47     rintro v ⟨⟨r,a,m⟩,rfl⟩
48     change TensorProduct.lift f (r ⊗ₜ[R] (a • m) - (r * ε a) ⊗ₜ[R] m) = 0
49     simpa only [map_sub, TensorProduct.lift.tmul, sub_eq_zero] using hf r a m)
50 
51 /-- The descended map evaluates pure tensors as prescribed. -/
52 theorem lift_tensorMk (ε : A →ₐ[R] R) (f : R →ₗ[R] M →ₗ[R] W)
53     (hf : ∀ r a m, f r (a • m) = f (r * ε a) m) (r : R) (m : M) :
54     lift ε f hf (tensorMk ε r m) = f r m := rfl
55 
56 /-- A map out of the balanced tensor product is determined by pure tensors. -/
57 theorem hom_ext (ε : A →ₐ[R] R) {f g : Tensor (M := M) ε →ₗ[R] W}
58     (h : ∀ r m, f (tensorMk ε r m) = g (tensorMk ε r m)) : f = g := by
59   apply Submodule.linearMap_qext
60   apply TensorProduct.ext'
61   intro r m
62   exact h r m
63 
64 /-- Existence and uniqueness give the full balanced tensor universal property. -/
65 theorem exists_unique_lift (ε : A →ₐ[R] R) (f : R →ₗ[R] M →ₗ[R] W)
66     (hf : ∀ r a m, f r (a • m) = f (r * ε a) m) :
67     ∃! F : Tensor (M := M) ε →ₗ[R] W, ∀ r m, F (tensorMk ε r m) = f r m := by
68   refine ⟨lift ε f hf, lift_tensorMk ε f hf, ?_⟩
69   intro F hF
70   exact hom_ext ε fun r m => (hF r m).trans (lift_tensorMk ε f hf r m).symm
71 
72 /-- Evaluate a balanced tensor in the augmentation coinvariants. -/
73 def toCoinvariants (ε : A →ₐ[R] R) :
74     Tensor (M := M) ε →ₗ[R] Coinvariants (M := M) ε :=
75   lift ε ((TensorProduct.mk R R M).compr₂
76     ((mk ε).comp (TensorProduct.lid R M).toLinearMap)) (by
77       intro r a m
78       change mk ε (r • (a • m)) = mk ε ((r * ε a) • m)
79       rw [map_smul, mk_smul, map_smul, smul_smul])
80 
81 /-- Tensor evaluation is coefficient multiplication in the quotient. -/
82 theorem toCoinvariants_tensorMk (ε : A →ₐ[R] R) (r : R) (m : M) :
83     toCoinvariants ε (tensorMk ε r m) = r • mk ε m := by
84   change mk ε (r • m) = r • mk ε m
85   exact map_smul (mk ε) r m
86 
87 /-- Send a coinvariant to the tensor of one with a representative. -/
88 def fromCoinvariants (ε : A →ₐ[R] R) :
89     Coinvariants (M := M) ε →ₗ[R] Tensor (M := M) ε :=
90   (relations ε).liftQ (tensorMk ε 1) (Submodule.span_le.mpr <| by
91     rintro v ⟨⟨a,m⟩,rfl⟩
92     change tensorMk ε 1 (a • m - ε a • m) = 0
93     rw [map_sub, (tensorMk ε 1).map_smul (ε a), sub_eq_zero,
94       tensorMk_balanced, one_mul]
95     exact tensorMk_scalar ε (ε a) m)
96 
97 /-- The quotient-to-tensor map uses the original representative. -/
98 theorem fromCoinvariants_mk (ε : A →ₐ[R] R) (m : M) :
99     fromCoinvariants ε (mk ε m) = tensorMk ε 1 m := rfl
100 
101 /-- Reconstructing and evaluating a coinvariant is the identity. -/
102 theorem to_from (ε : A →ₐ[R] R) :
103     (toCoinvariants (M := M) ε).comp (fromCoinvariants ε) = LinearMap.id := by
104   apply Submodule.linearMap_qext
105   ext m
106   change toCoinvariants ε (fromCoinvariants ε (mk ε m)) = mk ε m
107   rw [fromCoinvariants_mk, toCoinvariants_tensorMk, one_smul]
108 
109 /-- Evaluating and reconstructing a tensor is the identity. -/
110 theorem from_to (ε : A →ₐ[R] R) :
111     (fromCoinvariants (M := M) ε).comp (toCoinvariants ε) = LinearMap.id := by
112   apply hom_ext ε
113   intro r m
114   change fromCoinvariants ε (toCoinvariants ε (tensorMk ε r m)) = tensorMk ε r m
115   rw [toCoinvariants_tensorMk, map_smul, fromCoinvariants_mk]
116   exact (tensorMk_scalar ε r m).symm
117 
118 /-- Balanced tensor product equals the actual augmentation quotient. -/
119 def tensorEquivCoinvariants (ε : A →ₐ[R] R) :
120     Tensor (M := M) ε ≃ₗ[R] Coinvariants (M := M) ε :=
121   LinearEquiv.ofLinearMap (toCoinvariants ε) (fromCoinvariants ε) (to_from ε) (from_to ε)
122 
123 /-- A free A-module recovers exactly its original number of R-coordinates. -/
124 noncomputable def freeTensorEquiv [IsScalarTower R A M] {ι : Type*} [Fintype ι]
125     (ε : A →ₐ[R] R) (b : Module.Basis ι A M) : Tensor (M := M) ε ≃ₗ[R] (ι → R) :=
126   (tensorEquivCoinvariants ε).trans (freeEquiv ε b)
127 
128 end PaperXII.BalancedAugmentation

Back to source controls