diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
index 07b04957..007f2a63 100644
--- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
+++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
@@ -187,22 +187,6 @@ lemma _root_.IsDedekindDomain.HeightOneSpectrum.adicValued.continuous_algebraMap
     rw [mul_comm]
     exact Int.mul_le_of_le_ediv (by positivity) le_rfl
 
-/-- Say `w` is a finite place of `L` lying above `v` a finite place of `K`. Then there's a ring hom
-`K_v → L_w`. -/
-noncomputable def adicCompletionComapRingHom
-    (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) (hvw : v = comap A w) :
-    adicCompletion K v →+* adicCompletion L w :=
-  letI : UniformSpace K := v.adicValued.toUniformSpace;
-  letI : UniformSpace L := w.adicValued.toUniformSpace;
-  UniformSpace.Completion.mapRingHom (algebraMap K L) <| by
-  apply _root_.IsDedekindDomain.HeightOneSpectrum.adicValued.continuous_algebraMap A K L B v w hvw
-
-omit [IsIntegralClosure B A L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Module.Finite A B] in
-lemma adicCompletionComapRingHom_continuous
-    (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) (hvw : v = comap A w) :
-    Continuous (adicCompletionComapRingHom A K L B v w hvw) := by
-  convert UniformSpace.Completion.continuous_extension (β := (adicCompletion L w))
-
 noncomputable def adicCompletionComapSemialgHom (v : HeightOneSpectrum A) (w : HeightOneSpectrum B)
     (hvw : v = comap A w) :
     (HeightOneSpectrum.adicCompletion K v) →ₛₐ[algebraMap K L]
@@ -211,21 +195,28 @@ noncomputable def adicCompletionComapSemialgHom (v : HeightOneSpectrum A) (w : H
   letI : UniformSpace L := w.adicValued.toUniformSpace;
   UniformSpace.Completion.mapSemialgHom _ <|
   IsDedekindDomain.HeightOneSpectrum.adicValued.continuous_algebraMap A K L B v w hvw
-  -- commutes' r := by
-  --   subst hvw
-  --   simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
-  --     MonoidHom.coe_coe]
-  --   have : (adicCompletionComapRingHom A K _ w rfl) (algebraMap _ _ r)  =
-  --       (algebraMap L (adicCompletion L w)) (algebraMap K L r) := by
-  --     letI : UniformSpace L := w.adicValued.toUniformSpace
-  --     letI : UniformSpace K := (comap A w).adicValued.toUniformSpace
-  --     rw [adicCompletionComapRingHom, UniformSpace.Completion.mapRingHom]
-  --     apply UniformSpace.Completion.extensionHom_coe
-  --   rw [this, ← IsScalarTower.algebraMap_apply K L]
-  -- cont :=
-  --   letI : UniformSpace K := v.adicValued.toUniformSpace;
-  --   letI : UniformSpace L := w.adicValued.toUniformSpace;
-  --   UniformSpace.Completion.continuous_extension
+
+-- Do we even need to prove that this map is continuous? It will follow from
+-- the fact that it's K_v-linear once we know L_w has the K_v-module topology,
+-- which is the next lemma.
+-- omit [IsIntegralClosure B A L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
+--     [Module.Finite A B] in
+-- lemma adicCompletionComapSemialgHom_continuous
+--     (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) (hvw : v = comap A w) :
+--     Continuous (adicCompletionComapSemialgHom A K L B v w hvw) := by
+--   convert UniformSpace.Completion.continuous_extension (β := (adicCompletion L w))
+
+
+lemma adicCompletionComap_isModuleTopology
+    (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) (hvw : v = comap A w) :
+    -- temporarily make L_w a K_v-algebra
+    let inst_alg : Algebra (HeightOneSpectrum.adicCompletion K v)
+      (HeightOneSpectrum.adicCompletion L w) := RingHom.toAlgebra <|
+        adicCompletionComapSemialgHom A K L B v w hvw
+    -- the claim that L_w has the module topology.
+    IsModuleTopology (HeightOneSpectrum.adicCompletion K v)
+      (HeightOneSpectrum.adicCompletion L w) := by
+  sorry -- FLT#326
 
 omit [IsIntegralClosure B A L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
     [Module.Finite A B] in
@@ -234,7 +225,6 @@ lemma adicCompletionComapSemialgHom_coe
     adicCompletionComapSemialgHom A K L B v w hvw x = algebraMap K L x :=
   (adicCompletionComapSemialgHom A K L B v w hvw).commutes x
 
--- this name is surely wrong
 omit [IsIntegralClosure B A L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
     [Module.Finite A B] in
 open WithZeroTopology in
@@ -256,40 +246,67 @@ lemma v_adicCompletionComapSemialgHom
   subst hvw
   rw [← valuation_comap A K L B w a]
 
+/-- The canonical map `K_v → ∏_{w|v} L_w` extending K → L. -/
 noncomputable def adicCompletionComapSemialgHom' (v : HeightOneSpectrum A) :
   (HeightOneSpectrum.adicCompletion K v) →ₛₐ[algebraMap K L]
     (∀ w : {w : HeightOneSpectrum B // v = comap A w}, HeightOneSpectrum.adicCompletion L w.1) :=
   Pi.semialgHom _ _ fun i ↦ adicCompletionComapSemialgHom A K L B v i.1 i.2
 
-theorem adicCompletionComapSemialgHom_continuous (v : HeightOneSpectrum A) :
-    Continuous (adicCompletionComapSemialgHom' A K L B v) :=
-  continuous_pi fun w ↦ adicCompletionComapRingHom_continuous A K L B v w w.2
+lemma prodAdicCompletionComap_isModuleTopology
+    (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) (hvw : v = comap A w) :
+    -- temporarily make ∏_w L_w a K_v-algebra
+    let inst_alg : Algebra (HeightOneSpectrum.adicCompletion K v)
+      (∀ w : {w : HeightOneSpectrum B // v = comap A w}, HeightOneSpectrum.adicCompletion L w.1) :=
+      RingHom.toAlgebra <|
+        Pi.ringHom (fun w : {w : HeightOneSpectrum B // v = comap A w} ↦ adicCompletionComapSemialgHom A K L B v w.1 w.2)
+    -- the claim that L_w has the module topology.
+    IsModuleTopology (HeightOneSpectrum.adicCompletion K v)
+      (∀ w : {w : HeightOneSpectrum B // v = comap A w}, HeightOneSpectrum.adicCompletion L w.1) := by
+  sorry -- FLT#327
 
 open scoped TensorProduct -- ⊗ notation for tensor product
 
-/-
-
-A ---> B
-/\     /\
-|      |
-K ---> L
-
-L ⊗[K] A -> B
-
--/
-noncomputable def adicCompletionTensorComapAlgHom (v : HeightOneSpectrum A) :
+/-- The canonical L-algebra map `L ⊗_K K_v → ∏_{w|v} L_w`. -/
+noncomputable def tensorAdicCompletionComapAlgHom (v : HeightOneSpectrum A) :
     L ⊗[K] adicCompletion K v →ₐ[L]
       Π w : {w : HeightOneSpectrum B // v = comap A w}, adicCompletion L w.1 :=
   SemialgHom.baseChange_of_algebraMap (adicCompletionComapSemialgHom' A K L B v)
 
 omit [IsIntegralClosure B A L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
     [Module.Finite A B] in
-lemma adicCompletionComapAlgIso_tmul_apply (v : HeightOneSpectrum A) (x y i) :
-  adicCompletionTensorComapAlgHom A K L B v (x ⊗ₜ y) i =
+lemma tensorAdicCompletionComapAlgHom_tmul_apply (v : HeightOneSpectrum A) (x y i) :
+  tensorAdicCompletionComapAlgHom A K L B v (x ⊗ₜ y) i =
     x • adicCompletionComapSemialgHom A K L B v i.1 i.2 y := by
   rw [Algebra.smul_def]
   rfl
 
+theorem tensorAdicCompletionComapAlgHom_bijective (v : HeightOneSpectrum A) :
+    Function.Bijective (tensorAdicCompletionComapAlgHom A K L B v) := by
+  sorry -- issue FLT#231
+
+noncomputable def adicCompletionComapAlgEquiv (v : HeightOneSpectrum A) :
+  (L ⊗[K] (HeightOneSpectrum.adicCompletion K v)) ≃ₐ[L]
+    (∀ w : {w : HeightOneSpectrum B // v = comap A w}, HeightOneSpectrum.adicCompletion L w.1) :=
+  AlgEquiv.ofBijective (tensorAdicCompletionComapAlgHom A K L B v) <|
+    tensorAdicCompletionComapAlgHom_bijective A K L B v
+
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
+variable (v : HeightOneSpectrum A) in
+instance : TopologicalSpace (L ⊗[K] adicCompletion K v) := moduleTopology (adicCompletion K v) _
+
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
+variable (v : HeightOneSpectrum A) in
+instance : IsModuleTopology (adicCompletion K v) (L ⊗[K] adicCompletion K v) :=
+  ⟨rfl⟩
+
+noncomputable def adicCompletionComapContinuousAlgEquiv (v : HeightOneSpectrum A) :
+  (L ⊗[K] (HeightOneSpectrum.adicCompletion K v)) ≃A[L]
+    (∀ w : {w : HeightOneSpectrum B // v = comap A w}, HeightOneSpectrum.adicCompletion L w.1)
+  where
+    toAlgEquiv := adicCompletionComapAlgEquiv A K L B v
+    continuous_toFun := sorry -- FLT#328
+    continuous_invFun := sorry -- FLT#328
+
 attribute [local instance 9999] SMulCommClass.of_commMonoid TensorProduct.isScalarTower_left IsScalarTower.right
 
 instance (R K : Type*) [CommRing R] [IsDedekindDomain R] [Field K]
@@ -304,6 +321,7 @@ def adicCompletionIntegersSubalgebra {R : Type*} (K : Type*) [CommRing R]
   __ := HeightOneSpectrum.adicCompletionIntegers K v
   algebraMap_mem' r := coe_mem_adicCompletionIntegers v r
 
+/-- The canonical map `B ⊗[A] A_v → L ⊗[K] K_v` -/
 noncomputable def tensorAdicCompletionIntegersTo (v : HeightOneSpectrum A) :
     B ⊗[A] adicCompletionIntegers K v →ₐ[B] L ⊗[K] adicCompletion K v :=
   Algebra.TensorProduct.lift
@@ -316,7 +334,7 @@ omit [IsIntegralClosure B A L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
 set_option linter.deprecated false in -- `map_zero` and `map_add` time-outs
 theorem range_adicCompletionComapAlgIso_tensorAdicCompletionIntegersTo_le_pi
     (v : HeightOneSpectrum A) :
-    AlgHom.range (((adicCompletionTensorComapAlgHom A K L B v).restrictScalars B).comp
+    AlgHom.range (((tensorAdicCompletionComapAlgHom A K L B v).restrictScalars B).comp
       (tensorAdicCompletionIntegersTo A K L B v)) ≤
       Subalgebra.pi Set.univ (fun _ ↦ adicCompletionIntegersSubalgebra _ _) := by
   rintro _ ⟨x, rfl⟩ i -
@@ -325,14 +343,14 @@ theorem range_adicCompletionComapAlgIso_tensorAdicCompletionIntegersTo_le_pi
     Function.comp_apply, SetLike.mem_coe]
   induction' x with x y x y hx hy
   · rw [(tensorAdicCompletionIntegersTo A K L B v).map_zero,
-      (adicCompletionTensorComapAlgHom A K L B v).map_zero]
+      (tensorAdicCompletionComapAlgHom A K L B v).map_zero]
     exact zero_mem _
   · simp only [tensorAdicCompletionIntegersTo, Algebra.TensorProduct.lift_tmul, AlgHom.coe_comp,
       Function.comp_apply, Algebra.ofId_apply, AlgHom.commutes,
       Algebra.TensorProduct.algebraMap_apply, AlgHom.coe_restrictScalars',
       IsScalarTower.coe_toAlgHom', ValuationSubring.algebraMap_apply,
       Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul,
-      adicCompletionComapAlgIso_tmul_apply, algebraMap_smul]
+      tensorAdicCompletionComapAlgHom_tmul_apply, algebraMap_smul]
     apply Subalgebra.smul_mem
     show _ ≤ (1 : ℤₘ₀)
     rw [v_adicCompletionComapSemialgHom A K (L := L) (B := B) v i.1 i.2 y.1,
@@ -345,46 +363,13 @@ theorem range_adicCompletionComapAlgIso_tensorAdicCompletionIntegersTo_le_pi
         (algebraMap_injective_of_field_isFractionRing A B K L)).not.mpr
         (comap A i.1).3) i.1.2 Ideal.map_comap_le
   · rw [(tensorAdicCompletionIntegersTo A K L B v).map_add,
-      (adicCompletionTensorComapAlgHom A K L B v).map_add]
+      (tensorAdicCompletionComapAlgHom A K L B v).map_add]
     exact add_mem hx hy
 
-attribute [local instance] Algebra.TensorProduct.rightAlgebra in
-variable (v : HeightOneSpectrum A) in
-instance : TopologicalSpace (L ⊗[K] adicCompletion K v) := moduleTopology (adicCompletion K v) _
-
-attribute [local instance] Algebra.TensorProduct.rightAlgebra in
-variable (v : HeightOneSpectrum A) in
-instance : IsModuleTopology (adicCompletion K v) (L ⊗[K] adicCompletion K v) :=
-  ⟨rfl⟩
-
-attribute [local instance] Algebra.TensorProduct.rightAlgebra in
-noncomputable def adicCompletionTensorComapContinuousAlgHom (v : HeightOneSpectrum A) :
-    L ⊗[K] adicCompletion K v →A[L]
-      Π w : {w : HeightOneSpectrum B // v = comap A w}, adicCompletion L w.1 where
-  __ := adicCompletionTensorComapAlgHom A K L B v
-  cont := by
-    apply IsModuleTopology.continuous_of_ringHom (R := adicCompletion K v)
-    show Continuous (RingHom.comp _ (Algebra.TensorProduct.includeRight.toRingHom))
-    convert (adicCompletionComapSemialgHom_continuous A K L B v) using 1
-    ext kv w
-    simp [adicCompletionTensorComapAlgHom, adicCompletionComapSemialgHom_continuous,
-      SemialgHom.baseChange_of_algebraMap]
-    rfl
-
-noncomputable def adicCompletionComapAlgEquiv (v : HeightOneSpectrum A) :
-  (L ⊗[K] (HeightOneSpectrum.adicCompletion K v)) ≃ₐ[L]
-    (∀ w : {w : HeightOneSpectrum B // v = comap A w}, HeightOneSpectrum.adicCompletion L w.1) :=
-  AlgEquiv.ofBijective (adicCompletionTensorComapAlgHom A K L B v) sorry --#231
-
-noncomputable def adicCompletionComapContinuousAlgEquiv (v : HeightOneSpectrum A) :
-  (L ⊗[K] (HeightOneSpectrum.adicCompletion K v)) ≃A[L]
-    (∀ w : {w : HeightOneSpectrum B // v = comap A w}, HeightOneSpectrum.adicCompletion L w.1)
-  := sorry
-
 theorem adicCompletionComapAlgEquiv_integral : ∃ S : Finset (HeightOneSpectrum A), ∀ v ∉ S,
-  AlgHom.range (((adicCompletionTensorComapAlgHom A K L B v).restrictScalars B).comp
+    AlgHom.range (((tensorAdicCompletionComapAlgHom A K L B v).restrictScalars B).comp
       (tensorAdicCompletionIntegersTo A K L B v)) =
-      Subalgebra.pi Set.univ (fun _ ↦ adicCompletionIntegersSubalgebra _ _) := sorry
+    Subalgebra.pi Set.univ (fun _ ↦ adicCompletionIntegersSubalgebra _ _) := sorry -- FLT#329
 
 end IsDedekindDomain.HeightOneSpectrum
 
@@ -392,12 +377,6 @@ namespace DedekindDomain
 
 open IsDedekindDomain HeightOneSpectrum
 
-open scoped TensorProduct -- ⊗ notation for tensor product
-
--- Make ∏_w L_w into a K-algebra in a way compatible with the L-algebra structure
-variable [Algebra K (ProdAdicCompletions B L)]
-  [IsScalarTower K L (ProdAdicCompletions B L)]
-
 noncomputable def ProdAdicCompletions.baseChange :
     ProdAdicCompletions A K →ₛₐ[algebraMap K L] ProdAdicCompletions B L where
   toFun kv w := (adicCompletionComapSemialgHom A K L B _ w rfl (kv (comap A w)))
@@ -414,8 +393,12 @@ noncomputable def ProdAdicCompletions.baseChange :
     dsimp only
     funext w
     rw [Pi.add_apply, Pi.add_apply, map_add]
-  map_smul' := sorry
+  map_smul' k xv := by
+    apply funext
+    intro w
+    exact (adicCompletionComapSemialgHom A K L B _ w rfl).map_smul' k (xv (comap A w))
 
+open scoped TensorProduct -- ⊗ notation for tensor product
 
 -- Note that this is only true because L/K is finite; in general tensor product doesn't
 -- commute with infinite products, but it does here.
@@ -455,12 +438,9 @@ theorem ProdAdicCompletions.baseChangeEquiv_isFiniteAdele_iff' (x : ProdAdicComp
     rw [ProdAdicCompletions.baseChangeEquiv_isFiniteAdele_iff A K L B]
     exact h 1
 
--- Make ∏_w L_w into a K-algebra in a way compatible with the L-algebra structure
-variable [Algebra K (FiniteAdeleRing B L)]
-  [IsScalarTower K L (FiniteAdeleRing B L)]
-
 -- Restriction of an algebra map is an algebra map; these should be easy. #242
-noncomputable def FiniteAdeleRing.baseChange : FiniteAdeleRing A K →ₐ[K] FiniteAdeleRing B L where
+noncomputable def FiniteAdeleRing.baseChange :
+    FiniteAdeleRing A K →ₛₐ[algebraMap K L] 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' := by
@@ -478,40 +458,41 @@ noncomputable def FiniteAdeleRing.baseChange : FiniteAdeleRing A K →ₐ[K] Fin
     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
+  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, SemialgHom.commutes, i, j]
-
--- Presumably we have this?
-noncomputable def bar {K L AK AL : Type*} [CommRing K] [CommRing L]
-    [CommRing AK] [CommRing AL] [Algebra K AK] [Algebra K AL] [Algebra K L]
-    [Algebra L AL] [IsScalarTower K L AL]
-    (f : AK →ₐ[K] AL) : L ⊗[K] AK →ₐ[L] AL :=
-  Algebra.TensorProduct.lift (Algebra.ofId _ _) f <| fun l ak ↦ mul_comm (Algebra.ofId _ _ l) (f ak)
+  map_smul' k xv := by
+    refine ext B L <| funext fun w ↦ ?_
+    exact (adicCompletionComapSemialgHom A K L B _ w rfl).map_smul' k (xv (comap A w))
 
 noncomputable instance : Algebra (FiniteAdeleRing A K) (L ⊗[K] FiniteAdeleRing A K) :=
   Algebra.TensorProduct.rightAlgebra
 
+noncomputable
+instance BaseChange.algebra : Algebra (FiniteAdeleRing A K) (FiniteAdeleRing B L) :=
+  RingHom.toAlgebra (FiniteAdeleRing.baseChange A K L B)
+
+lemma BaseChange.isModuleTopology : IsModuleTopology (FiniteAdeleRing A K) (FiniteAdeleRing B L) :=
+  sorry
+
 instance : TopologicalSpace (L ⊗[K] FiniteAdeleRing A K) :=
   moduleTopology (FiniteAdeleRing A K) (L ⊗[K] FiniteAdeleRing A K)
 -- Follows from the above. Should be a continuous L-alg equiv but we don't have continuous
 -- alg equivs yet so can't even state it properly.
-noncomputable def FiniteAdeleRing.baseChangeEquiv :
+noncomputable def FiniteAdeleRing.baseChangeAlgEquiv :
+    L ⊗[K] FiniteAdeleRing A K ≃ₐ[L] FiniteAdeleRing B L where
+  __ := AlgEquiv.ofBijective
+    (SemialgHom.baseChange_of_algebraMap <| FiniteAdeleRing.baseChange A K L B)
+    -- ⊢ Function.Bijective ⇑(baseChange A K L B).baseChange_of_algebraMap
+    sorry -- #243
+
+noncomputable def FiniteAdeleRing.baseChangeContinuousAlgEquiv :
     L ⊗[K] FiniteAdeleRing A K ≃A[L] FiniteAdeleRing B L where
-  __ := AlgEquiv.ofBijective (bar <| FiniteAdeleRing.baseChange A K L B) sorry -- #243
-  continuous_toFun := sorry -- TODO
-  continuous_invFun := sorry -- TODO
+  __ := FiniteAdeleRing.baseChangeAlgEquiv A K L B
+  continuous_toFun := sorry
+  continuous_invFun := sorry
+
 
 end DedekindDomain
diff --git a/FLT/Mathlib/Algebra/Algebra/Bilinear.lean b/FLT/Mathlib/Algebra/Algebra/Bilinear.lean
index cf887423..011fb69a 100644
--- a/FLT/Mathlib/Algebra/Algebra/Bilinear.lean
+++ b/FLT/Mathlib/Algebra/Algebra/Bilinear.lean
@@ -2,9 +2,13 @@ import Mathlib
 import FLT.Mathlib.Algebra.Algebra.Hom
 
 variable {R S : Type*} [CommSemiring R] [CommSemiring S] {φ : R →+* S}
-    {A B : Type*}  [CommSemiring A] [Semiring B] [Algebra R A] [Algebra S B]
+    {A B : Type*}  [Semiring A] [Semiring B] [Algebra R A] [Algebra S B]
 
 open scoped TensorProduct in
+/-- Given S an R-algebra, and a ring homomorphism `ψ` from an R-algebra A to an S-algebra B
+compatible with the algebra map R → S, `baseChange_of_algebraMap ψ` is the induced
+`S`-algebra map `S ⊗[R] A → B`.
+-/
 noncomputable
 def SemialgHom.baseChange_of_algebraMap [Algebra R S] (ψ : A →ₛₐ[algebraMap R S] B) :
     S ⊗[R] A →ₐ[S] B :=
diff --git a/blueprint/lean_decls b/blueprint/lean_decls
index 08a7eb78..0463e80b 100644
--- a/blueprint/lean_decls
+++ b/blueprint/lean_decls
@@ -60,11 +60,15 @@ AutomorphicForm.GLn.AutomorphicFormForGLnOverQ
 NumberField.AdeleRing.locallyCompactSpace
 IsDedekindDomain.HeightOneSpectrum.valuation_comap
 IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom
+IsDedekindDomain.HeightOneSpectrum.adicCompletionComap_isModuleTopology
+IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom'
 IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv
+IsDedekindDomain.HeightOneSpectrum.prodAdicCompletionComap_isModuleTopology
+IsDedekindDomain.HeightOneSpectrum.adicCompletionComapContinuousAlgEquiv
 IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv_integral
 DedekindDomain.ProdAdicCompletions.baseChange
 DedekindDomain.FiniteAdeleRing.baseChange
-DedekindDomain.FiniteAdeleRing.baseChangeEquiv
+DedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv
 NumberField.InfiniteAdeleRing.baseChangeEquiv
 NumberField.AdeleRing.baseChangeEquiv
 Rat.AdeleRing.zero_discrete
diff --git a/blueprint/src/chapter/AdeleMiniproject.tex b/blueprint/src/chapter/AdeleMiniproject.tex
index f4edad8a..de26ad32 100644
--- a/blueprint/src/chapter/AdeleMiniproject.tex
+++ b/blueprint/src/chapter/AdeleMiniproject.tex
@@ -114,8 +114,11 @@ \subsection{Base change for finite adeles}
 the height one spectrum of $A$.
 
 Now let~$L/K$ be a finite separable extension, and let $B$ be the integral closure of~$A$ in~$L$.
-If $w$ is a nonzero prime ideal of $B$ lying under $v$, a prime ideal of $A$, then we can put the
-$w$-adic topology on $L$ and the $v$-adic topology on~$K$. Furthermore
+We want to relate the finite adeles of $K$ and of $L$. We work place by place, starting by fixing
+one place upstairs and analysing its relation to the place downstairs.
+
+So let $w$ be a nonzero prime ideal of $B$. Say $w$ lies over $v$, a prime ideal of $A$.
+Then we can put the $w$-adic topology on $L$ and the $v$-adic topology on~$K$. Furthermore
 we can equip $K$ with an additive $v$-adic valuation, that is,
 a function also called $v$ fron $K$ to $\Z\cup\{\infty\}$ normalised so that if $\pi$ is a uniformiser
 for $v$ then $v(\pi)=1$. Similarly we consider $w$ as a function from $L$ to $\Z\cup\{\infty\}$.
@@ -137,22 +140,55 @@ \subsection{Base change for finite adeles}
   \label{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom}
   \uses{IsDedekindDomain.HeightOneSpectrum.valuation_comap}
   \leanok
-  There's a natural continuous $K$-algebra homomorphism map $K_v\to L_w$. It is defined by completing
+  There's a natural ring map $K_v\to L_w$ extending the map $K\to L$.
+  It is defined by completing
   the inclusion $K\to L$ at the finite places $v$ and $w$ (which can be done
   because the previous lemma shows that the map is uniformly continuous for the $v$-adic
   and $w$-adic topologies).
 \end{definition}
 
-Now say $v$ is in the height one spectrum of $A$. The map above induces a continuous
-$K$-algebra homomorphism $K_v\to\prod_{w|v}L_w$, where the product runs over the height one
-primes of $B$ which pull back to $v$.
+\begin{theorem}
+  \lean{IsDedekindDomain.HeightOneSpectrum.adicCompletionComap_isModuleTopology}
+  \label{IsDedekindDomain.HeightOneSpectrum.adicCompletionComap_isModuleTopology}
+  \uses{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom}
+  \leanok
+  Giving $L_w$ the $K_v$-module structure coming from the natural map $K_v\to L_w$,
+  the $w$-adic topology on $L_w$ is the $K_v$-module topology.
+\end{theorem}
+\begin{proof}
+  Any basis for $L$ as a $K$-vector space spans $L_w$ as a $K_v$-module, so $L_w$ is
+  finite-dimensional over $K_v$ and the module topology is the same as the product
+  topology. So we need to establish that the product topology on $L_w=K_v^n$ is
+  the $w$-adic topology. But the $w$-adic topology is induced by the $w$-adic norm,
+  which makes $L_w$ into a normed $K_v$-vector space, and (after picking a basis)
+  the product norm on $L_w=K_v^n$ also makes $L_w$ into a normed $K_v$-vector space.
+  So the result follows from the standard fact (see for example the lemma on p52
+  of Cassels-Froelich) that any two norms on a finite-dimensional vector space over
+  a complete field are equivalent (and thus induce the same topology).
+\end{proof}
+
+Now instead of fixing $w$ upstairs, we fix $v$ downstairs. So say $v$ is in the height one
+spectrum of $A$.
+
+\begin{definition}
+  \lean{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom'}
+  \label{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom'}
+  \uses{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom}
+  \leanok
+  The product of the maps $K_v\to L_w$ for $w|v$ is a natural ring map $K_v\to\prod_{w|v}L_w$
+  lying over $K\to L$. Here the product runs over the height one primes of $B$ which pull back to $v$.
+\end{definition}
+
+Because $K_v\to\prod_{w|v}L_w$ lies over $K\to L$, there's an induced $L$-algebra
+map $L\otimes_KK_v\to\prod_{w|v}L_w$.
 
 \begin{theorem}
   \lean{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv}
   \label{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv}
-  \uses{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom}
-  The induced continuous $L$-algebra homomorphism $L\otimes_KK_v\to\prod_{w|v}L_w$ is an
-  isomorphism (both algebraic and topological).
+  \uses{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom'}
+  \leanok
+  The induced $L$-algebra homomorphism $L\otimes_KK_v\to\prod_{w|v}L_w$ is an
+  isomorphism of rings.
 \end{theorem}
 \begin{proof}
   We follow Theorem 5.12 on p21 of \href{https://math.berkeley.edu/~ltomczak/notes/Mich2022/LF_Notes.pdf}
@@ -178,11 +214,40 @@ \subsection{Base change for finite adeles}
   of $K_v$, and the image is dense because $L$ is dense in $L_w$, hence $L_i=L_w$.
 \end{proof}
 
+\begin{theorem}
+  \label{IsDedekindDomain.HeightOneSpectrum.prodAdicCompletionComap_isModuleTopology}
+  \lean{IsDedekindDomain.HeightOneSpectrum.prodAdicCompletionComap_isModuleTopology}
+  \uses{IsDedekindDomain.HeightOneSpectrum.adicCompletionComap_isModuleTopology}
+  \leanok
+  For $v$ fixed, the product topology on $\prod_{w|v}L_w$ is the $K_v$-module
+  topology.
+\end{theorem}
+\begin{proof}
+  This is a finite product of $K_v$-modules each of which has the $K_v$-module topology
+  by~\ref{IsDedekindDomain.HeightOneSpectrum.adicCompletionComap_isModuleTopology},
+  and the product topology is the module topology for a finite product of modules each of which
+  has the module topology (this is in mathlib).
+\end{proof}
+
+\begin{theorem}
+  \label{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapContinuousAlgEquiv}
+  \lean{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapContinuousAlgEquiv}
+  \uses{IsDedekindDomain.HeightOneSpectrum.prodAdicCompletionComap_isModuleTopology}
+  If we give $L\otimes_KK_v$ the $K_v$-module topology then the $L$-algebra isomorphism
+  $L\otimes_K K_v\cong\prod_{w|v}L_w$ is also a homeomorphism.
+\end{theorem}
+\begin{proof} Indeed, is a $K_v$-algebra isomorphism between two modules each of which
+  have the module topology, and any module map is automorphically continuous for the
+  module topologies.
+\end{proof}
+
+We now start thinking about what's going on at the integral level.
+
 \begin{theorem}
   \lean{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv_integral}
   \label{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv_integral}
   \uses{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv}
-  The isomorphism $L\otimes_KK_v\to\prod_{w|v}L_w$ induces a topological isomorphism
+  The isomorphism $L\otimes_KK_v\to\prod_{w|v}L_w$ induces an isomorphism
   $B\otimes_AA_v\to \prod_{w|v}B_w$
   for all but finitely many $v$ in the height one spectrum of $A$.
 \end{theorem}
@@ -220,7 +285,7 @@ \subsection{Base change for finite adeles}
 Note that we make no claim about continuity; such a claim wouldn't help
 us because the adeles do not get the subspace topology.
 
-\begin{theorem} This map induces a natural continuous $K$-algebra homomorphism
+\begin{theorem} This map induces a natural $K$-algebra homomorphism
   $\A_{A,K}^\infty\to\A_{B,L}^\infty$.
   \label{DedekindDomain.FiniteAdeleRing.baseChange}
   \lean{DedekindDomain.FiniteAdeleRing.baseChange}
@@ -230,14 +295,12 @@ \subsection{Base change for finite adeles}
   This does not need the hard direction of
   theorem~\ref{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv_integral}.
   the definition of the map is straightforward using only that integers map
-  to integers. Continuity also follows from this property; the induction function from
-  $\prod_v A_v$ to $\prod_w B_w$ is continuous, and this gives continuity
-  of the map at zero, and hence continuity everywhere.
+  to integers.
 \end{proof}
 
 \begin{theorem}
-  \label{DedekindDomain.FiniteAdeleRing.baseChangeEquiv}
-  \lean{DedekindDomain.FiniteAdeleRing.baseChangeEquiv}
+  \label{DedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv}
+  \lean{DedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv}
   \uses{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv_integral}
   \leanok
   If we give $L\otimes_K\A_{A,K}^\infty$ the ``module topology'', coming from the fact
@@ -250,10 +313,14 @@ \subsection{Base change for finite adeles}
   theorem~\ref{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv_integral}.
   Surjectivity follows from
   theorem~\ref{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv_integral}.
-  The fact that it is a topological isomorphism follows from the fact that
+  The fact that it is a topological isomorphism surely follows from the fact that
   $L\otimes_K K_v=\oplus_{w|v}L_w$ and that this identification identifies
   the subgroup $\calO_L\otimes_K K_v$ with $\oplus_{w|v}\calO_{L_w}$ for all
-  but finitely many $v$.
+  but finitely many $v$. Although I'm wondering whether it's easier to prove
+  that the map $\A_{A,K}^\infty\to\A_{B,L}^\infty$ makes $\A_{B,L}^\infty$
+  into an $\A_{A,K}^\infty$-module and the claim (also undoubtedly true, although
+  I am not sure of the best level of abstractionhere ) that the topology on
+  $\A_{B,L}^\infty$ is the $\A_{A,K}^\infty$-module topology.
 \end{proof}
 
 \subsection{Base change for infinite adeles}
diff --git a/blueprint/src/chapter/HaarCharacterProject.tex b/blueprint/src/chapter/HaarCharacterProject.tex
index dd0832fb..0f649803 100644
--- a/blueprint/src/chapter/HaarCharacterProject.tex
+++ b/blueprint/src/chapter/HaarCharacterProject.tex
@@ -311,7 +311,7 @@ \section{Adeles}
 \begin{proof} If $u=(u_v)$ as $v$ runs through the places of $K$ then
   $d_{B_{\A}}(\ell_u)=\prod_v d_{B_v}(\ell_{u_v})$ by
   theorem~\ref{addHaarScalarFactor_restricted_product} (and the product is finite).
-  By corollary~\cite{distribHaarChar_eq_addHaarScalarFactor_right_of_isCentralSimple}
+  By corollary~\ref{distribHaarChar_eq_addHaarScalarFactor_right_of_isCentralSimple}
   this equals $\prod_v d_{B_v}(r_{u_v})$, and again by
   theorem~\ref{addHaarScalarFactor_restricted_product} this is $d_{B_{\A}}(r_u)$.
 \end{proof}