Skip to content

Commit abf5c56

Browse files
chrisflavchrisflav
committed
fix
1 parent ff1103b commit abf5c56

3 files changed

Lines changed: 59 additions & 40 deletions

File tree

‎Mathlib/RingTheory/AdicCompletion/Algebra.lean‎

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -55,19 +55,24 @@ def transitionMapₐ {m n : ℕ} (hmn : m ≤ n) :
5555
R ⧸ (I ^ n • ⊤ : Ideal R) →ₐ[R] R ⧸ (I ^ m • ⊤ : Ideal R) :=
5656
AlgHom.ofLinearMap (transitionMap I R hmn) rfl (transitionMap_map_mul I hmn)
5757

58-
instance : Mul (AdicCompletion I R) where
59-
mul x y := ⟨x.val * y.val, by simp [x.property, y.property]⟩
58+
/-- `AdicCompletion I R` is an `R`-subalgebra of `∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)`. -/
59+
def subalgebra : Subalgebra R (∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)) :=
60+
Submodule.toSubalgebra (submodule I R) (fun _ ↦ by simp)
61+
(fun x y hx hy m n hmn ↦ by simp [hx hmn, hy hmn])
6062

61-
instance : One (AdicCompletion I R) where
62-
one := ⟨1, by simp⟩
63+
/-- `AdicCompletion I R` is a subring of `∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)`. -/
64+
def subring : Subring (∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)) :=
65+
Subalgebra.toSubring (subalgebra I)
6366

67+
/-- One in `AdicCompletion I R`. -/
6468
@[irreducible]
6569
def one : AdicCompletion I R :=
6670
⟨1, by simp⟩
6771

6872
instance : One (AdicCompletion I R) where
6973
one := one I
7074

75+
/-- Multiplication in `AdicCompletion I R`. -/
7176
@[irreducible]
7277
def mul (x y : AdicCompletion I R) : AdicCompletion I R :=
7378
⟨x.val * y.val, by simp [x.property, y.property]⟩
@@ -100,6 +105,7 @@ instance : CommRing (AdicCompletion I R) where
100105
sub_eq_add_neg x y := Subtype.ext <| sub_eq_add_neg x.val y.val
101106
mul_comm x y := Subtype.ext <| mul_comm x.val y.val
102107

108+
/-- Function of `R`-algebra map of `AdicCompletion I R`. -/
103109
@[irreducible]
104110
def algebraMapFun (r : R) : AdicCompletion I R :=
105111
⟨algebraMap R (∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)) r, by simp⟩
@@ -155,13 +161,15 @@ def subalgebra : Subalgebra R (ℕ → R) :=
155161
def subring : Subring (ℕ → R) :=
156162
Subalgebra.toSubring (AdicCauchySequence.subalgebra I)
157163

164+
/-- One in `AdicCauchySequence I R`. -/
158165
@[irreducible]
159166
def one : AdicCauchySequence I R :=
160167
⟨1, fun _ ↦ rfl⟩
161168

162169
instance : One (AdicCauchySequence I R) where
163170
one := one I
164171

172+
/-- Multiplication in `AdicCauchySequence I R`. -/
165173
@[irreducible]
166174
def mul (x y : AdicCauchySequence I R) : AdicCauchySequence I R :=
167175
⟨x.val * y.val, fun hmn ↦ SModEq.mul (x.property hmn) (y.property hmn)⟩
@@ -194,6 +202,7 @@ instance : CommRing (AdicCauchySequence I R) where
194202
sub_eq_add_neg x y := Subtype.ext <| sub_eq_add_neg x.val y.val
195203
mul_comm x y := Subtype.ext <| mul_comm x.val y.val
196204

205+
/-- Function of `R`-algebra map of `AdicCauchySequence I R`. -/
197206
@[irreducible]
198207
def algebraMapFun (r : R) : AdicCauchySequence I R :=
199208
⟨algebraMap R (∀ _, R) r, fun _ ↦ rfl⟩
@@ -281,6 +290,7 @@ instance : IsScalarTower R (R ⧸ (I • ⊤ : Ideal R)) (M ⧸ (I • ⊤ : Sub
281290
rw [← Submodule.Quotient.mk_smul, Ideal.Quotient.mk_eq_mk, mk_smul_mk, smul_assoc]
282291
rfl
283292

293+
/-- `AdicCompletion I R`-scalar multiplication on `AdicCompletion I M`. -/
284294
@[irreducible]
285295
def smul' (r : AdicCompletion I R) (x : AdicCompletion I M) : AdicCompletion I M where
286296
val := fun n ↦ eval I R n r • eval I M n x

‎Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean‎

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -44,9 +44,8 @@ def ofTensorProductBil : AdicCompletion I R →ₗ[AdicCompletion I R] M →ₗ[
4444
map_smul' r x := by
4545
apply LinearMap.ext
4646
intro y
47-
simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply,
48-
LinearMap.lsmul_apply, RingHom.id_apply, LinearMap.smul_apply]
49-
rw [smul_eq_mul, mul_smul]
47+
ext n
48+
simp [mul_smul (r.val n)]
5049

5150
@[simp]
5251
private lemma ofTensorProductBil_apply_apply (r : AdicCompletion I R) (x : M) :
@@ -83,10 +82,11 @@ variable (ι : Type*) [Fintype ι] [DecidableEq ι]
8382
private lemma piEquivOfFintype_comp_ofTensorProduct_eq :
8483
piEquivOfFintype I (fun _ : ι ↦ R) ∘ₗ ofTensorProduct I (ι → R) =
8584
(TensorProduct.piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).toLinearMap := by
86-
ext i j k
87-
suffices h : (if j = i then 1 else 0) = (if j = i then 1 else 0 : AdicCompletion I R).val k by
88-
simpa [Pi.single_apply, -smul_eq_mul, -Algebra.id.smul_eq_mul]
89-
split <;> simp only [smul_eq_mul, val_zero, val_one]
85+
ext x i j k
86+
suffices h : (if j = i then (Ideal.Quotient.mk (I ^ k • ⊤)) (x.val k) • 1 else 0) =
87+
(if j = i then (mk I R) x else 0).val k by
88+
simpa [-smul_eq_mul, -Algebra.id.smul_eq_mul, Pi.single_apply]
89+
split <;> simp
9090

9191
private lemma ofTensorProduct_eq :
9292
ofTensorProduct I (ι → R) = (piEquivOfFintype I (ι := ι) (fun _ : ι ↦ R)).symm.toLinearMap ∘ₗ
@@ -130,6 +130,8 @@ lemma ofTensorProduct_bijective_of_pi_of_fintype :
130130

131131
end PiFintype
132132

133+
unseal smul' in
134+
unseal mul in
133135
/-- If `M` is a finite `R`-module, then the canonical map
134136
`AdicCompletion I R ⊗[R] M →ₗ AdicCompletion I M` is surjective. -/
135137
lemma ofTensorProduct_surjective_of_fg [Module.Finite R M] :

‎Mathlib/RingTheory/AdicCompletion/Basic.lean‎

Lines changed: 36 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -204,37 +204,52 @@ end IsPrecomplete
204204

205205
namespace AdicCompletion
206206

207+
/-- `AdicCompletion` is the submodule of compatible families in
208+
`∀ n : ℕ, M ⧸ (I ^ n • ⊤)`. -/
209+
def submodule : Submodule R (∀ n : ℕ, M ⧸ (I ^ n • ⊤ : Submodule R M)) where
210+
carrier := { f | ∀ {m n} (hmn : m ≤ n), AdicCompletion.transitionMap I M hmn (f n) = f m }
211+
zero_mem' hmn := by rw [Pi.zero_apply, Pi.zero_apply, LinearMap.map_zero]
212+
add_mem' hf hg m n hmn := by
213+
rw [Pi.add_apply, Pi.add_apply, LinearMap.map_add, hf hmn, hg hmn]
214+
smul_mem' c f hf m n hmn := by rw [Pi.smul_apply, Pi.smul_apply, LinearMap.map_smul, hf hmn]
215+
216+
/-- Zero of `AdicCompletion I M`. -/
207217
@[irreducible]
208218
def zero : AdicCompletion I M := ⟨0, by simp⟩
209219

210220
instance : Zero (AdicCompletion I M) where
211221
zero := zero I M
212222

223+
/-- Addition in `AdicCompletion I M`. -/
213224
@[irreducible]
214225
def add (x y : AdicCompletion I M) : AdicCompletion I M :=
215226
⟨x.val + y.val, by simp [x.property, y.property]⟩
216227

217228
instance : Add (AdicCompletion I M) where
218229
add := add I M
219230

231+
/-- Negation in `AdicCompletion I M`. -/
220232
@[irreducible]
221233
def neg (x : AdicCompletion I M) : AdicCompletion I M :=
222234
⟨- x.val, by simp [x.property]⟩
223235

224236
instance : Neg (AdicCompletion I M) where
225237
neg := neg I M
226238

239+
/-- Subtraction in `AdicCompletion I M`. -/
227240
@[irreducible]
228241
def sub (x y : AdicCompletion I M) : AdicCompletion I M :=
229242
⟨x.val - y.val, by simp [x.property, y.property]⟩
230243

231244
instance : Sub (AdicCompletion I M) where
232245
sub := sub I M
233246

247+
/-- Natural scalar multiplication in `AdicCompletion I M`. -/
234248
@[irreducible]
235249
def nsmul (n : ℕ) (x : AdicCompletion I M) : AdicCompletion I M :=
236250
nsmulRec n x
237251

252+
/-- Integer scalar multiplication in `AdicCompletion I M`. -/
238253
@[irreducible]
239254
def zsmul (n : ℤ) (x : AdicCompletion I M) : AdicCompletion I M :=
240255
zsmulRec (nsmul I M) n x
@@ -255,6 +270,7 @@ instance : AddCommGroup (AdicCompletion I M) where
255270
add_left_neg a := Subtype.ext <| add_left_neg a.val
256271
add_comm x y := Subtype.ext <| add_comm x.val y.val
257272

273+
/-- Scalar multiplication in `AdicCompletion I M`. -/
258274
@[irreducible]
259275
def smul (r : R) (x : AdicCompletion I M) : AdicCompletion I M :=
260276
⟨r • x.val, by simp [x.property]⟩
@@ -424,67 +440,57 @@ def AdicCauchySequence : Type _ := { f : ℕ → M // IsAdicCauchy I M f }
424440

425441
namespace AdicCauchySequence
426442

427-
instance : Zero (AdicCauchySequence I M) where
428-
zero := ⟨0, fun _ ↦ rfl⟩
429-
430-
instance : Add (AdicCauchySequence I M) where
431-
add x y := ⟨x.val + y.val, fun hmn ↦ SModEq.add (x.property hmn) (y.property hmn)⟩
432-
433-
instance : Neg (AdicCauchySequence I M) where
434-
neg x := ⟨- x.val, fun hmn ↦ SModEq.neg (x.property hmn)⟩
435-
436-
instance : AddCommGroup (AdicCauchySequence I M) where
437-
add_assoc x y z := Subtype.ext <| add_assoc x.val y.val z.val
438-
sub x y := ⟨x.val - y.val, fun hmn ↦ SModEq.sub (x.property hmn) (y.property hmn)⟩
439-
sub_eq_add_neg x y := Subtype.ext <| sub_eq_add_neg x.val y.val
440-
zero_add a := Subtype.ext <| zero_add a.val
441-
add_zero a := Subtype.ext <| add_zero a.val
442-
nsmul := nsmulRec
443-
zsmul := zsmulRec
444-
add_left_neg a := Subtype.ext <| add_left_neg a.val
445-
add_comm x y := Subtype.ext <| add_comm x.val y.val
446-
447-
instance : Module R (AdicCauchySequence I M) where
448-
smul r x := ⟨r • x.val, fun hmn ↦ SModEq.smul (x.property hmn) r⟩
449-
one_smul x := Subtype.ext <| one_smul R x.val
450-
mul_smul r s x := Subtype.ext <| mul_smul r s x.val
451-
smul_add r x y := Subtype.ext <| smul_add r x.val y.val
452-
add_smul r s x := Subtype.ext <| add_smul r s x.val
453-
zero_smul x := Subtype.ext <| zero_smul R x.val
454-
smul_zero r := Subtype.ext <| smul_zero r
455-
443+
/-- The type of `I`-adic cauchy sequences is a submodule of the product `ℕ → M`. -/
444+
def submodule : Submodule R (ℕ → M) where
445+
carrier := { f | IsAdicCauchy I M f }
446+
add_mem' := by
447+
intro f g hf hg m n hmn
448+
exact SModEq.add (hf hmn) (hg hmn)
449+
zero_mem' := by
450+
intro _ _ _
451+
rfl
452+
smul_mem' := by
453+
intro r f hf m n hmn
454+
exact SModEq.smul (hf hmn) r
455+
456+
/-- Zero in `AdicCauchySequence I M`. -/
456457
@[irreducible]
457458
def zero : AdicCauchySequence I M :=
458459
⟨0, fun _ ↦ rfl⟩
459460

460461
instance : Zero (AdicCauchySequence I M) where
461462
zero := zero I M
462463

464+
/-- Addition in `AdicCauchySequence I M`. -/
463465
@[irreducible]
464466
def add (x y : AdicCauchySequence I M) : AdicCauchySequence I M :=
465467
⟨x.val + y.val, fun hmn ↦ SModEq.add (x.property hmn) (y.property hmn)⟩
466468

467469
instance : Add (AdicCauchySequence I M) where
468470
add := add I M
469471

472+
/-- Negation in `AdicCauchySequence I M`. -/
470473
@[irreducible]
471474
def neg (x : AdicCauchySequence I M) : AdicCauchySequence I M :=
472475
⟨- x.val, fun hmn ↦ SModEq.neg (x.property hmn)⟩
473476

474477
instance : Neg (AdicCauchySequence I M) where
475478
neg := neg I M
476479

480+
/-- Subtraction in `AdicCauchySequence I M`. -/
477481
@[irreducible]
478482
def sub (x y : AdicCauchySequence I M) : AdicCauchySequence I M :=
479483
⟨x.val - y.val, fun hmn ↦ SModEq.sub (x.property hmn) (y.property hmn)⟩
480484

481485
instance : Sub (AdicCauchySequence I M) where
482486
sub := sub I M
483487

488+
/-- Natural scalar multiplication in `AdicCauchySequence I M`. -/
484489
@[irreducible]
485490
def nsmul (n : ℕ) (x : AdicCauchySequence I M) : AdicCauchySequence I M :=
486491
nsmulRec n x
487492

493+
/-- Integer scalar multiplication in `AdicCauchySequence I M`. -/
488494
@[irreducible]
489495
def zsmul (n : ℤ) (x : AdicCauchySequence I M) : AdicCauchySequence I M :=
490496
zsmulRec (nsmul I M) n x
@@ -505,6 +511,7 @@ instance : AddCommGroup (AdicCauchySequence I M) where
505511
add_left_neg a := Subtype.ext <| add_left_neg a.val
506512
add_comm x y := Subtype.ext <| add_comm x.val y.val
507513

514+
/-- Scalar multiplication in `AdicCauchySequence I M`. -/
508515
@[irreducible]
509516
def smul (r : R) (x : AdicCauchySequence I M) : AdicCauchySequence I M :=
510517
⟨r • x.val, fun hmn ↦ SModEq.smul (x.property hmn) r⟩

0 commit comments

Comments
 (0)