BaseChange.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

30 declarations, 0 contain sorry, 0 declared as axioms

Base change of adele rings.

If A is a Dedekind domain with field of fractions K, if L/K is a finite separable extension and if B is the integral closure of A in L, then B is also a Dedekind domain. Hence the rings of finite adeles 𝔸_K^∞ and 𝔸_L^∞ (defined using A and B) are defined. In this file we define the natural K-algebra map 𝔸_K^∞ → 𝔸_L^∞ and the natural L-algebra map 𝔸_K^∞ ⊗[K] L → 𝔸_L^∞, and show that the latter map is an isomorphism.

Main definitions

FiniteAdeleRing.baseChangeAlgEquiv : L ⊗[K] 𝔸ᶠ[A, K] ≃ₐ[L] 𝔸ᶠ[B, L]

Main theorems

𝔸ᶠ[B, L] has the 𝔸ᶠ[A, K]-module topology, shown as an instance.

Imports (11)

Imported by 2 files

lemma IsDedekindDomain.tendsTo_comap_cofinite line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, IsDedekindDomain, Module.Finite, FaithfulSMul, Filter.Tendsto, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.under, Filter.cofinite
Proof uses: FractionRing, nonZeroDivisors, Filter.Tendsto.cofinite_of_finite_preimage_singleton, IsDedekindDomain.HeightOneSpectrum.Extension.finite, FractionRing.liftAlgebra
40 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.cofinite_mapsTo_adicCompletionSemialgHom line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, Filter.Eventually, IsDedekindDomain.HeightOneSpectrum, Set.MapsTo, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.HeightOneSpectrum.under, Eq, Subtype.mk, rfl, SemialgHom, Algebra.algebraMap, IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers and 1 more
Proof uses: Filter.Eventually.of_forall, Iff.mp, LE.le, Set, Set.image, Subring, ValuationSubring.toSubring, Set.preimage, Set.image_subset_iff, IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom_image_adicCompletionIntegers
43 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.FiniteAdeleRing.mapRingHom The ring homomorphism 𝔸_K^∞ → 𝔸_L^∞ for L/K an extension of number fields line 75 source
Source documentation
The ring homomorphism 𝔸_K^∞ → 𝔸_L^∞ for L/K an extension of number fields.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, RingHom, IsDedekindDomain.FiniteAdeleRing
Proof uses: FaithfulSMul, RestrictedProduct.mapAlongRingHom, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Filter.cofinite, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.under, IsDedekindDomain.tendsTo_comap_cofinite, SemialgHom, Algebra.algebraMap, Eq, Subtype.mk, IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom, IsDedekindDomain.cofinite_mapsTo_adicCompletionSemialgHom
34 instances, coercions and auxiliary constants left out.
```
noncomputable def mapRingHom : 𝔸ᶠ[A, K] →+* 𝔸ᶠ[B, L] :=
…
```
def IsDedekindDomain.FiniteAdeleRing.mapSemialgHom The ring homomorphism 𝔸_K^∞ → 𝔸_L^∞ for L/K an extension of number fields, as a morphism lying over the canonical map K → L line 83 source
Source documentation
The ring homomorphism 𝔸_K^∞ → 𝔸_L^∞ for L/K an extension of number fields, as a morphism lying over the canonical map K → L.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, ContinuousSemialgHom, Algebra.algebraMap, IsDedekindDomain.FiniteAdeleRing
Proof uses: RingHom, IsDedekindDomain.FiniteAdeleRing.mapRingHom, ContinuousSemialgHom.mk, SemialgHom.mk, LinearMap.mk, AddHom.mk, OneHom.toFun
36 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def mapSemialgHom :
    𝔸ᶠ[A, K] →SA[algebraMap K L] 𝔸ᶠ[B, L] where
…
```
lemma IsDedekindDomain.FiniteAdeleRing.mapSemialgHom_apply line 97 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.HeightOneSpectrum, Eq, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ContinuousSemialgHom, Algebra.algebraMap, IsDedekindDomain.FiniteAdeleRing.mapSemialgHom, SemialgHom, IsDedekindDomain.HeightOneSpectrum.under, Subtype.mk, rfl, IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom
34 instances, coercions and auxiliary constants left out.
instance IsDedekindDomain.FiniteAdeleRing.(instance at line 104) line 104 source
class IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul Utility class which specialises RestrictedProduct.FiberwiseSMul to the case of finite adele rings line 111 source
Source documentation
Utility class which specialises RestrictedProduct.FiberwiseSMul to the case of finite adele rings.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, IsDedekindDomain.FiniteAdeleRing
8 instances, coercions and auxiliary constants left out.
```
class ComapFiberwiseSMul extends RestrictedProduct.FiberwiseSMul (α := HeightOneSpectrum B)
…
```
Mentions: RestrictedProduct.FiberwiseSMul
theorem IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul.map_smul' line 119 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.Extension, Eq, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.HeightOneSpectrum.under, HSMul.hSMul
Proof uses: RestrictedProduct.FiberwiseSMul.map_smul, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, Subtype, RestrictedProduct
39 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.FiniteAdeleRing.BaseChange.algebraMap_apply line 124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, IsDedekindDomain.HeightOneSpectrum, Eq, IsDedekindDomain.HeightOneSpectrum.adicCompletion, RingHom, Algebra.algebraMap, SemialgHom, IsDedekindDomain.HeightOneSpectrum.under, Subtype.mk, rfl, IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HSMul.hSMul, OfNat.ofNat, congrFun, Algebra.algebraMap_eq_smul_one, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul.map_smul', RingHom.toAlgebra, SemialgHom.toRingHom, HMul.hMul, mul_one, eq_self
57 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.FiniteAdeleRing.tensorEquivTensor The canonical linear isomorphism L ⊗[K] 𝔸_K^∞ ≅ B ⊗[A] 𝔸_K^∞ line 133 source
Source documentation
The canonical linear isomorphism L ⊗[K] 𝔸_K^∞ ≅ B ⊗[A] 𝔸_K^∞.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, FiniteDimensional, LinearEquiv, RingHom.id, TensorProduct, IsDedekindDomain.FiniteAdeleRing
Proof uses: IsDedekindDomain.linearEquivTensorProductModuleLeft
37 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def tensorEquivTensor [FiniteDimensional K L] : L ⊗[K] 𝔸ᶠ[A, K] ≃ₗ[B] B ⊗[A] 𝔸ᶠ[A, K] := by
…
```
lemma IsDedekindDomain.FiniteAdeleRing.tensorEquivTensor_tmul line 137 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, FiniteDimensional, IsDedekindDomain.FiniteAdeleRing, Eq, TensorProduct, LinearEquiv, RingHom.id, IsDedekindDomain.FiniteAdeleRing.tensorEquivTensor, TensorProduct.tmul, RingHom, Algebra.algebraMap
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, IsDedekindDomain.linearEquivTensorProductModuleLeft_tmul, eq_self
53 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.FiniteAdeleRing.tensorEquivRestrictedProduct The B-linear isomorphism φ : B ⊗[K] 𝔸_K^∞ ≅ ∏'_v [B ⊗[A] K_v, B ⊗[A] 𝓞_v] given by φ (b ⊗ x) v = b ⊗ (x v) line 143 source
Source documentation
The B-linear isomorphism φ : B ⊗[K] 𝔸_K^∞ ≅ ∏'_v [B ⊗[A] K_v, B ⊗[A] 𝓞_v] given by φ (b ⊗ x) v = b ⊗ (x v).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, LinearEquiv, RingHom.id, TensorProduct, IsDedekindDomain.FiniteAdeleRing, RestrictedProduct, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Submodule, RestrictedProduct.rangeLTensorLeft, IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerSubmodule, Filter.cofinite
Proof uses: Module.FinitePresentation, Module.IsTorsionFree, RestrictedProduct.lTensorEquivLeft, LinearEquiv.trans, TensorProduct.AlgebraTensorModule.congr, LinearEquiv.refl, AddEquiv, AddEquiv.refl, LinearEquiv.mk, LinearMap.mk, AddHom.mk, Equiv.toFun, AddEquiv.toEquiv, Equiv.invFun
65 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
def tensorEquivRestrictedProduct : B ⊗[A] 𝔸ᶠ[A, K] ≃ₗ[B] Πʳ v, [B ⊗[A] (adicCompletion K v),
    RestrictedProduct.rangeLTensorLeft A B (adicCompletion K) (integerSubmodule K) v] := by
…
```
Mentions: RestrictedProduct.rangeLTensorLeft
lemma IsDedekindDomain.FiniteAdeleRing.tensorEquivRestrictedProduct_tmul line 158 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.HeightOneSpectrum, Eq, TensorProduct, IsDedekindDomain.HeightOneSpectrum.adicCompletion, RestrictedProduct, Submodule, RestrictedProduct.rangeLTensorLeft, IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerSubmodule, Filter.cofinite, LinearEquiv, RingHom.id, IsDedekindDomain.FiniteAdeleRing.tensorEquivRestrictedProduct and 1 more
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, RestrictedProduct.lTensorEquivLeft_tmul, eq_self
61 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.FiniteAdeleRing.restrictedProductTensorProductEquivRestrictedProductProd The B-linear isomorphism ∏'_v [B ⊗[A] K_v, B ⊗[A] 𝓞_v] ≅ ∏'_v [∏_{w|v} L_w, ∏_{w|v} 𝓞_w] given by adicCompletionComapIntegerLinearEquiv line 165 source
Source documentation
The B-linear isomorphism ∏'_v [B ⊗[A] K_v, B ⊗[A] 𝓞_v] ≅ ∏'_v [∏_{w|v} L_w, ∏_{w|v} 𝓞_w] given by adicCompletionComapIntegerLinearEquiv.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, FiniteDimensional, LinearEquiv, RingHom.id, RestrictedProduct, IsDedekindDomain.HeightOneSpectrum, TensorProduct, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Submodule, RestrictedProduct.rangeLTensorLeft, IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerSubmodule, Filter.cofinite, IsDedekindDomain.HeightOneSpectrum.Extension, Eq and 3 more
Proof uses: LinearEquiv.restrictedProductCongrRight, IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquiv
57 instances, coercions and auxiliary constants left out.
```
def restrictedProductTensorProductEquivRestrictedProductProd [FiniteDimensional K L] :
    Πʳ v, [B ⊗[A] (adicCompletion K v),
      RestrictedProduct.rangeLTensorLeft A B (adicCompletion K) (integerSubmodule K) v] ≃ₗ[B]
    Πʳ (v : HeightOneSpectrum A), [(w : Extension B v) → adicCompletion L w.val,
      Submodule.pi Set.univ fun w : Extension B v ↦ (integerSubmodule L w.val)] :=
…
```
Mentions: RestrictedProduct.rangeLTensorLeft
lemma IsDedekindDomain.FiniteAdeleRing.restrictedProduct_tensorProduct_equiv_restrictedProduct_prod_apply line 175 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, FiniteDimensional, RestrictedProduct, IsDedekindDomain.HeightOneSpectrum, TensorProduct, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Submodule, RestrictedProduct.rangeLTensorLeft, IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerSubmodule, Filter.cofinite, Eq, IsDedekindDomain.HeightOneSpectrum.Extension, IsDedekindDomain.HeightOneSpectrum.under, Submodule.pi and 6 more
Proof uses: rfl
68 instances, coercions and auxiliary constants left out.
def IsDedekindDomain.FiniteAdeleRing.restrictedProductProdEquiv The B-linear isomorphism ∏'_v [∏_{w|v} L_w, ∏_{w|v} 𝓞_w] → 𝔸_L^∞ given by RestrictedProduct.flattenEquiv' line 183 source
Source documentation
The B-linear isomorphism ∏'_v [∏_{w|v} L_w, ∏_{w|v} 𝓞_w] → 𝔸_L^∞ given by RestrictedProduct.flattenEquiv'.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, LinearEquiv, RingHom.id, RestrictedProduct, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.Extension, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, IsDedekindDomain.HeightOneSpectrum.under, Submodule, Submodule.pi, Set.univ, IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerSubmodule, Filter.cofinite and 1 more
Proof uses: FaithfulSMul, Equiv, Set.preimage, Singleton.singleton, Set, Membership.mem, Set.pi, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, RestrictedProduct.flattenEquiv', IsDedekindDomain.tendsTo_comap_cofinite, LinearEquiv.mk, LinearMap.mk, AddHom.mk, Equiv.toFun, Equiv.invFun
62 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def restrictedProductProdEquiv :
    Πʳ (v : HeightOneSpectrum A), [(w : Extension B v) → adicCompletion L w.val,
      Submodule.pi .univ fun w : Extension B v ↦ (integerSubmodule L w.val)] ≃ₗ[B]
    𝔸ᶠ[B, L] :=
…
```
lemma IsDedekindDomain.FiniteAdeleRing.restrictedProduct_prod_equiv_apply line 201 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, RestrictedProduct, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.Extension, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, IsDedekindDomain.HeightOneSpectrum.under, Submodule, Submodule.pi, Set.univ, IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerSubmodule, Filter.cofinite, IsDedekindDomain.FiniteAdeleRing, LinearEquiv and 4 more
59 instances, coercions and auxiliary constants left out.
def IsDedekindDomain.FiniteAdeleRing.baseChangeLinearEquiv The L-linear isomorphism L ⊗ A_K^∞ ≅ A_L^∞ given by composing the previous four maps line 205 source
Source documentation
The L-linear isomorphism L ⊗ A_K^∞ ≅ A_L^∞ given by composing the previous four maps.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, FiniteDimensional, LinearEquiv, RingHom.id, TensorProduct, IsDedekindDomain.FiniteAdeleRing
Proof uses: IsDedekindDomain.FiniteAdeleRing.tensorEquivTensor, RestrictedProduct, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Submodule, RestrictedProduct.rangeLTensorLeft, IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerSubmodule, Filter.cofinite, IsDedekindDomain.FiniteAdeleRing.tensorEquivRestrictedProduct, IsDedekindDomain.HeightOneSpectrum.Extension, Eq, IsDedekindDomain.HeightOneSpectrum.under, Submodule.pi, Set.univ, IsDedekindDomain.FiniteAdeleRing.restrictedProductTensorProductEquivRestrictedProductProd, IsDedekindDomain.FiniteAdeleRing.restrictedProductProdEquiv, LinearEquiv.trans, LinearEquiv.extendScalarsOfIsLocalization, nonZeroDivisors
58 instances, coercions and auxiliary constants left out.
```
def baseChangeLinearEquiv [FiniteDimensional K L] : L ⊗[K] 𝔸ᶠ[A, K] ≃ₗ[L] 𝔸ᶠ[B, L] :=
…
```
lemma IsDedekindDomain.FiniteAdeleRing.algebraMap_apply_eq_algebraMap line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, Algebra, IsFractionRing, IsDedekindDomain, IsDedekindDomain.HeightOneSpectrum, Eq, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.FiniteAdeleRing, RingHom, Algebra.algebraMap
Proof uses: rfl
23 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.FiniteAdeleRing.baseChangeLinearEquiv_tmul line 218 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, FiniteDimensional, Eq, LinearEquiv, RingHom.id, TensorProduct, IsDedekindDomain.FiniteAdeleRing.baseChangeLinearEquiv, TensorProduct.tmul, RingHom, Algebra.algebraMap, HMul.hMul
Proof uses: IsDedekindDomain.FiniteAdeleRing.ext, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq.mpr, Valuation.Completion, WithZero, Multiplicative, Int, IsDedekindDomain.HeightOneSpectrum.valuation, IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion, WithVal, IsDedekindDomain.HeightOneSpectrum.under, Subtype.mk, rfl, WithVal.toVal, SemialgHom, IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom, id, congr and 29 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem IsDedekindDomain.FiniteAdeleRing.baseChange_bijective line 229 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, FiniteDimensional, Function.Bijective, TensorProduct, AlgHom, SemialgHom.baseChangeOfAlgebraMap, ContinuousSemialgHom.toSemialgHom, Algebra.algebraMap, IsDedekindDomain.FiniteAdeleRing.mapSemialgHom
Proof uses: Eq, SemialgHomClass.toSemialgHom, ContinuousSemialgHom, LinearEquiv, RingHom.id, IsDedekindDomain.FiniteAdeleRing.baseChangeLinearEquiv, Eq.mpr, LinearMap, AlgHom.toLinearMap, id, congrArg, Eq.symm, AlgHom.coe_toLinearMap, LinearEquiv.coe_toLinearMap, congr_arg, LinearMap.ext, TensorProduct.inductionOn, IsDedekindDomain.FiniteAdeleRing.ext, TensorProduct.tmul, IsDedekindDomain.HeightOneSpectrum and 47 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv The L-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞ line 256 source
Source documentation
The L-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, FiniteDimensional, AlgEquiv, TensorProduct
Proof uses: AlgEquiv.ofBijective, SemialgHom.baseChangeOfAlgebraMap, SemialgHomClass.toSemialgHom, ContinuousSemialgHom, Algebra.algebraMap, IsDedekindDomain.FiniteAdeleRing.mapSemialgHom, IsDedekindDomain.FiniteAdeleRing.baseChange_bijective
35 instances, coercions and auxiliary constants left out.
```
def baseChangeAlgEquiv [FiniteDimensional K L] :
    L ⊗[K] 𝔸ᶠ[A, K] ≃ₐ[L] 𝔸ᶠ[B, L] :=
…
```
def IsDedekindDomain.FiniteAdeleRing.baseChangeAdeleAlgEquiv The 𝔸_K^∞-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞ line 262 source
Source documentation
The 𝔸_K^∞-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, FiniteDimensional, AlgEquiv, TensorProduct, TensorProduct.RightActions.instAlgebra_fLT
Proof uses: AlgHom, RingHom.toAlgebra, SemialgHom.toRingHom, Algebra.algebraMap, ContinuousSemialgHom.toSemialgHom, IsDedekindDomain.FiniteAdeleRing.mapSemialgHom, SemialgHom.baseChangeRightOfAlgebraMap, IsDedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv, AlgEquiv.mk, Equiv.mk, OneHom.toFun, AlgHom.toRingHom, Equiv.invFun, AlgEquiv.toEquiv
42 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def baseChangeAdeleAlgEquiv [FiniteDimensional K L] :
    L ⊗[K] 𝔸ᶠ[A, K] ≃ₐ[𝔸ᶠ[A, K]] 𝔸ᶠ[B, L] where
…
```
instance IsDedekindDomain.FiniteAdeleRing.(instance at line 272) line 272 source
def IsDedekindDomain.FiniteAdeleRing.piAdicIntegerSubmodule ∏_{w∣v} 𝓞_w as an 𝓞_v-submodule of ∏_{w∣v} L_w line 294 source
Source documentation
∏_{w∣v} 𝓞_w as an 𝓞_v-submodule of ∏_{w∣v} L_w

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, IsDedekindDomain.HeightOneSpectrum, Submodule, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.Extension, Eq, IsDedekindDomain.HeightOneSpectrum.under, IsDedekindDomain.FiniteAdeleRing.instModuleSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersForallValHeightOneSpectrumEqUnder
Proof uses: Module, Module.compHom, Algebra.algebraMap, Submodule.pi, Set.univ, Subring, ValuationSubring.toSubring, Subring.toSubmodule, Submodule.restrictScalars, Algebra.mk, SMul.mk, HMul.hMul, RingHom, IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionIntegersRingHom
68 instances, coercions and auxiliary constants left out.
```
noncomputable def piAdicIntegerSubmodule (v : HeightOneSpectrum A) :
    Submodule (adicCompletionIntegers K v) ((w : Extension B v) → adicCompletion L w.val) :=
…
```
def IsDedekindDomain.FiniteAdeleRing.restrictedProductPiEquiv The continuous 𝔸 K-Linear equivalence between ∏'_v ∏_{w∣v} L_w and 𝔸 L given by reaindexing the elements line 319 source
Source documentation
The continuous 𝔸 K-Linear equivalence between ∏'_v ∏_{w∣v} L_w and 𝔸 L given by reaindexing the elements.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, ContinuousLinearEquiv, RingHom.id, RestrictedProduct, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.Extension, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, IsDedekindDomain.HeightOneSpectrum.under, Submodule, Subtype, Membership.mem and 6 more
Proof uses: FaithfulSMul, Homeomorph, RestrictedProduct.flattenHomeomorph', IsDedekindDomain.tendsTo_comap_cofinite, ContinuousLinearEquiv.mk, LinearEquiv.mk, LinearMap.mk, AddHom.mk, Equiv.toFun, Homeomorph.toEquiv, Equiv.invFun
67 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
noncomputable def restrictedProductPiEquiv :
    Πʳ (v : HeightOneSpectrum A), [(w : Extension B v) → adicCompletion L w.val,
      piAdicIntegerSubmodule A K L B v] ≃L[𝔸ᶠ[A, K]] 𝔸ᶠ[B, L] :=
…
```
Mentions: IsDedekindDomain.FiniteAdeleRing.piAdicIntegerSubmodule
lemma IsDedekindDomain.FiniteAdeleRing.restrictedProduct_pi_isModuleTopology line 336 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, FiniteDimensional, IsModuleTopology, RestrictedProduct, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.Extension, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, IsDedekindDomain.HeightOneSpectrum.under, Submodule, Subtype, Membership.mem and 6 more
Proof uses: Module.Finite.equiv, RingHom.id, ContinuousLinearEquiv.symm, IsDedekindDomain.FiniteAdeleRing.restrictedProductPiEquiv, RestrictedProduct.isModuleTopology, WithZero, Multiplicative, Int, Valued.isOpen_integer, Eq.mpr, IsOpen, Set.pi, Set.univ, Subring, ValuationSubring.toSubring, Subring.toSubmodule, id, congrArg, Set, Submodule.coe_pi and 15 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
instance IsDedekindDomain.FiniteAdeleRing.(instance at line 350) line 350 source
def IsDedekindDomain.FiniteAdeleRing.baseChangeAdeleContinuousAlgEquiv The continuous 𝔸_K^∞-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞ line 357 source
Source documentation
The continuous 𝔸_K^∞-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, FiniteDimensional, ContinuousAlgEquiv, TensorProduct, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, TensorProduct.RightActions.instAlgebra_fLT
Proof uses: IsModuleTopology.continuousAlgEquivOfAlgEquiv, IsDedekindDomain.FiniteAdeleRing.baseChangeAdeleAlgEquiv
30 instances, coercions and auxiliary constants left out.
```
noncomputable def baseChangeAdeleContinuousAlgEquiv [FiniteDimensional K L] :
    L ⊗[K] 𝔸ᶠ[A, K] ≃A[𝔸ᶠ[A, K]] 𝔸ᶠ[B, L] :=
…
```
def IsDedekindDomain.FiniteAdeleRing.baseChangeContinuousAlgEquiv The continuous L-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞ line 362 source
Source documentation
The continuous L-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Module.Finite, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, FiniteDimensional, ContinuousAlgEquiv, TensorProduct, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT
Proof uses: AlgEquiv, IsDedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv, TensorProduct.RightActions.instAlgebra_fLT, IsDedekindDomain.FiniteAdeleRing.baseChangeAdeleContinuousAlgEquiv, ContinuousAlgEquiv.mk
36 instances, coercions and auxiliary constants left out.
```
noncomputable def baseChangeContinuousAlgEquiv [FiniteDimensional K L] :
    L ⊗[K] 𝔸ᶠ[A, K] ≃A[L] 𝔸ᶠ[B, L] where
…
```