Definition of map A_K^f -> A_L^f (#269)

* First attempt * Cleaning * Minor idiomatic changes * Update FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Co-authored-by: Kevin Buzzard <[email protected]> * Update FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Co-authored-by: Kevin Buzzard <[email protected]> * Update FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Co-authored-by: Kevin Buzzard <[email protected]> * Update FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Co-authored-by: Kevin Buzzard <[email protected]> * Update FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Co-authored-by: Kevin Buzzard <[email protected]> * Tidying up * Resolving merging stupidity * Update FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Co-authored-by: Kevin Buzzard <[email protected]> * Update FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Co-authored-by: Kevin Buzzard <[email protected]> --------- Co-authored-by: Kevin Buzzard <[email protected]>
ImperialCollegeLondon · Dec 8, 2024 · a01a431 · a01a431
1 parent 0bffc11
commit a01a431
Showing 1 changed file with 31 additions and 5 deletions.
diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
@@ -451,11 +451,37 @@ variable [Algebra K (FiniteAdeleRing B L)]
 noncomputable def FiniteAdeleRing.baseChange : FiniteAdeleRing A K →ₐ[K] FiniteAdeleRing B L where
   toFun ak := ⟨ProdAdicCompletions.baseChange A K L B ak.1,
     (ProdAdicCompletions.baseChange_isFiniteAdele_iff A K L B ak).1 ak.2⟩
-  map_one' := sorry
-  map_mul' := sorry
-  map_zero' := sorry
-  map_add' := sorry
-  commutes' := sorry
+  map_one' := by
+    ext
+    have h : (1 : FiniteAdeleRing A K) = (1 : ProdAdicCompletions A K) := rfl
+    have t : (1 : FiniteAdeleRing B L) = (1 : ProdAdicCompletions B L) := rfl
+    simp_rw [h, t, map_one]
+  map_mul' x y := by
+    have h : (x * y : FiniteAdeleRing A K) =
+      (x : ProdAdicCompletions A K) * (y : ProdAdicCompletions A K) := rfl
+    simp_rw [h, map_mul]
+    rfl
+  map_zero' := by
+    ext
+    have h : (0 : FiniteAdeleRing A K) = (0 : ProdAdicCompletions A K) := rfl
+    have t : (0 : FiniteAdeleRing B L) = (0 : ProdAdicCompletions B L) := rfl
+    simp_rw [h, t, map_zero]
+  map_add' x y:= by
+    have h : (x + y : FiniteAdeleRing A K) =
+      (x : ProdAdicCompletions A K) + (y : ProdAdicCompletions A K) := rfl
+    simp_rw [h, map_add]
+    rfl
+  commutes' r := by
+    ext
+    have h : (((algebraMap K (FiniteAdeleRing A K)) r) : ProdAdicCompletions A K) =
+      (algebraMap K (ProdAdicCompletions A K)) r := rfl
+    have i : algebraMap K (FiniteAdeleRing B L) r =
+      algebraMap L (FiniteAdeleRing B L) (algebraMap K L r) :=
+      IsScalarTower.algebraMap_apply K L (FiniteAdeleRing B L) r
+    have j (p : L) : (((algebraMap L (FiniteAdeleRing B L)) p) : ProdAdicCompletions B L) =
+      (algebraMap L (ProdAdicCompletions B L)) p := rfl
+    simp_rw [h, AlgHom.commutes, i, j]
+    exact IsScalarTower.algebraMap_apply K L (ProdAdicCompletions B L) r
 
 -- Presumably we have this?
 noncomputable def bar {K L AK AL : Type*} [CommRing K] [CommRing L]