RightAugmentation.lean

1 import PaperXII.BalancedAugmentation
2 import Mathlib.Algebra.Algebra.Opposite
3 
4 set_option autoImplicit false
5 
6 /-! Right-module convention for M ⊗[A,ε] R, including noncommutative A.
7 The construction is the same full balanced quotient with its two inputs flipped.
8 The right action on M is represented by an Aᵐᵒᵖ-module structure. -/
9 namespace PaperXII.RightAugmentation
10 
11 open scoped TensorProduct
12 open MulOpposite
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 /-- Augmentation on the opposite algebra. -/
18 def oppositeAugmentation (ε : A →ₐ[R] R) : Aᵐᵒᵖ →ₐ[R] R :=
19   ε.fromOpposite fun _ _ => Commute.all _ _
20 
21 /-- The right balanced tensor M ⊗[A,ε] R. -/
22 abbrev Tensor (ε : A →ₐ[R] R) :=
23   BalancedAugmentation.Tensor (M := M) (oppositeAugmentation ε)
24 
25 /-- The conventional order of the two tensor inputs. -/
26 def tensorMk (ε : A →ₐ[R] R) : M →ₗ[R] R →ₗ[R] Tensor (M := M) ε :=
27   (BalancedAugmentation.tensorMk (oppositeAugmentation ε)).flip
28 
29 /-- The full right-module balancing equation. -/
30 theorem tensorMk_balanced (ε : A →ₐ[R] R) (a : A) (m : M) (r : R) :
31     tensorMk ε (op a • m) r = tensorMk ε m (ε a * r) := by
32   change BalancedAugmentation.tensorMk (oppositeAugmentation ε) r (op a • m) =
33     BalancedAugmentation.tensorMk (oppositeAugmentation ε) (ε a * r) m
34   rw [BalancedAugmentation.tensorMk_balanced]
35   change BalancedAugmentation.tensorMk (oppositeAugmentation ε) (r * ε a) m = _
36   rw [mul_comm]
37 
38 /-- Right balanced bilinear maps factor uniquely through this tensor. -/
39 theorem exists_unique_lift {W : Type*} [AddCommGroup W] [Module R W]
40     (ε : A →ₐ[R] R) (f : M →ₗ[R] R →ₗ[R] W)
41     (hf : ∀ a m r, f (op a • m) r = f m (ε a * r)) :
42     ∃! F : Tensor (M := M) ε →ₗ[R] W, ∀ m r, F (tensorMk ε m r) = f m r := by
43   have h : ∀ r (a : Aᵐᵒᵖ) m,
44       f.flip r (a • m) = f.flip (r * oppositeAugmentation ε a) m := by
45     intro r a m
46     change f (a • m) r = f m (r * ε a.unop)
47     simpa only [op_unop, mul_comm] using hf a.unop m r
48   obtain ⟨F,hF,hunique⟩ := BalancedAugmentation.exists_unique_lift
49     (oppositeAugmentation ε) f.flip h
50   refine ⟨F, fun m r => hF r m, ?_⟩
51   intro Q hQ
52   exact hunique Q fun r m => hQ m r
53 
54 /-- The actual augmentation ideal acts from the right. -/
55 def augmentationSMul (ε : A →ₐ[R] R) : Submodule R M :=
56   Submodule.span R {v | ∃ a : A, ε a = 0 ∧ ∃ m : M, op a • m = v}
57 
58 /-- Opposite-algebra notation preserves exactly the right ideal-action submodule. -/
59 theorem opposite_augmentationSMul (ε : A →ₐ[R] R) :
60     AugmentationCoinvariants.augmentationSMul (M := M) (oppositeAugmentation ε) =
61       augmentationSMul ε := by
62   unfold AugmentationCoinvariants.augmentationSMul augmentationSMul
63   apply congrArg (Submodule.span R)
64   ext v
65   constructor
66   · rintro ⟨a,ha,m,hm⟩
67     exact ⟨a.unop,ha,m,by simpa only [op_unop] using hm⟩
68   · rintro ⟨a,ha,m,hm⟩
69     exact ⟨op a,ha,m,hm⟩
70 
71 /-- The right tensor is exactly M divided by its augmentation-ideal action. -/
72 def tensorEquivQuotient [IsScalarTower R Aᵐᵒᵖ M] (ε : A →ₐ[R] R) :
73     Tensor (M := M) ε ≃ₗ[R] (M ⧸ augmentationSMul (M := M) ε) :=
74   (BalancedAugmentation.tensorEquivCoinvariants (oppositeAugmentation ε)).trans
75     (Submodule.quotEquivOfEq _ _
76       ((AugmentationCoinvariants.relations_eq_augmentationSMul (M := M)
77         (oppositeAugmentation ε)).trans (opposite_augmentationSMul (M := M) ε)))
78 
79 /-- The free right-module theorem retains every basis index. -/
80 noncomputable def freeEquiv [IsScalarTower R Aᵐᵒᵖ M] {ι : Type*} [Fintype ι]
81     (ε : A →ₐ[R] R) (b : Module.Basis ι Aᵐᵒᵖ M) :
82     Tensor (M := M) ε ≃ₗ[R] (ι → R) :=
83   BalancedAugmentation.freeTensorEquiv (oppositeAugmentation ε) b
84 
85 /-- A recovered basis with the same index set as the original right basis. -/
86 noncomputable def recoveredBasis [IsScalarTower R Aᵐᵒᵖ M] {ι : Type*} [Fintype ι]
87     (ε : A →ₐ[R] R) (b : Module.Basis ι Aᵐᵒᵖ M) :
88     Module.Basis ι R (Tensor (M := M) ε) :=
89   (Pi.basisFun R ι).map (freeEquiv ε b).symm
90 
91 end PaperXII.RightAugmentation

Back to source controls