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

59 declarations, 0 contain sorry, 0 declared as axioms

Base change of adic completions.

If A is a Dedekind domain with field of fractions K, if L/K is a finite extension and if B/A is also finite then L ⊗_K K_v ≅ ∏_{w|v} L_w as L-algebras. Further this map is continuous, K_v-linear and restricts to an isomorphism B ⊗_A 𝓞_v ≅ ∏_{w|v} 𝓞_w.

Main definitions

IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeContinuousAlgEquiv : L ⊗[K] K_v ≃A[L] ∏_{w|v} L_w

Main theorems

IsDedekindDomain.HeightOneSpectrum.Extension.valued_adicCompletionSemialgHom A K L B v w pf : If w|v are nonzero primes of B and A, and if x ∈ K_v ⊆ L_w, then w(x)=v(x)^e where e is the global ramification index of w/v.
IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChange_bijective A K L B v : The canonical map L ⊗ Kᵥ → ∏_{w|v} L_w is bijective.

Imports (16)

Imported by 3 files

example (example at line 84) line 84 source
example (example at line 89) line 89 source
example (example at line 91) line 91 source
example (example at line 94) line 94 source
example (example at line 97) line 97 source
example (example at line 102) line 102 source
lemma IsDedekindDomain.HeightOneSpectrum.adicValued.continuous_algebraMap line 125 source

def IsDedekindDomain.HeightOneSpectrum.Extension._root_.WithVal.semialgebraMap The map (R,v) → (S,w) as a semialgebra map over R → S (which is the same map!) line 172 source

Source documentation

The map (R,v) → (S,w) as a semialgebra map over R → S (which is the same map!).

def _root_.WithVal.semialgebraMap {R S Γ₀ Γ₀' : Type*} [CommRing R]
    [CommRing S] [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀']
    [Algebra R S] (v : Valuation R Γ₀) (w : Valuation S Γ₀') :
    WithVal v →ₛₐ[algebraMap R S] WithVal w where
…

def IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom If w of L divides v of K, underSemialgHom v w pf is the canonical map Kᵥ → L_w lying above K → L line 182 source
Source documentation
If w of L divides v of K, underSemialgHom v w pf is the canonical map Kᵥ → L_w lying above K → L. Here we actually use the type synonyms WithVal K and WithVal L.
```
noncomputable def adicCompletionSemialgHom :
    v.adicCompletion K →ₛₐ[algebraMap K L] w.1.adicCompletion L :=
…
```
lemma IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom_coe The square with sides K → K_v → L_w and K → L → L_w commutes line 191 source
Source documentation
The square with sides K → K_v → L_w and K → L → L_w commutes.
```
lemma adicCompletionSemialgHom_coe (x : WithVal (v.valuation K)) :
    w.adicCompletionSemialgHom K L x = algebraMap K L x.ofVal :=
…
```
lemma IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom_continuous The map K_v → L_w is continuous line 196 source
Source documentation
The map K_v → L_w is continuous.
```
lemma adicCompletionSemialgHom_continuous : Continuous (w.adicCompletionSemialgHom K L) :=
…
```
lemma IsDedekindDomain.HeightOneSpectrum.Extension.valued_adicCompletionSemialgHom The local ramification index for the extension L_w/K_v is equal to the global ramification index for the extension w/v line 206 source
Source documentation
The local ramification index for the extension L_w/K_v is equal to the global ramification index for the extension w/v. In other words, if x in K_v and i:K_v->L_w then w(i(x))=v(x)^e where e is computed globally.
```
lemma valued_adicCompletionSemialgHom (x) :
    Valued.v (adicCompletionSemialgHom K L w x) = Valued.v x ^
      w.1.asIdeal.ramificationIdx A := by
…
```
Mentions: IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom
lemma IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom_image_adicCompletionIntegers The canonical map K_v → L_w sends 𝓞_v to 𝓞_w line 227 source
Source documentation
The canonical map K_v → L_w sends 𝓞_v to 𝓞_w.
```
lemma adicCompletionSemialgHom_image_adicCompletionIntegers :
    w.adicCompletionSemialgHom K L '' (v.adicCompletionIntegers K) ⊆
      w.1.adicCompletionIntegers L := by
…
```
instance IsDedekindDomain.HeightOneSpectrum.Extension.(instance at line 238) line 238 source
instance IsDedekindDomain.HeightOneSpectrum.Extension.(instance at line 242) line 242 source
Source documentation
The K_v-action on L_w is continuous.
```
instance : ContinuousSMul (adicCompletion K v) (adicCompletion L w.1) := by
…
```
def IsDedekindDomain.HeightOneSpectrum.adicCompletion.semialgHomPi The canonical map K_v → ∏_{w|v} L_w extending K → L line 254 source
Source documentation
The canonical map K_v → ∏_{w|v} L_w extending K → L.
```
noncomputable def semialgHomPi :
    v.adicCompletion K →ₛₐ[algebraMap K L] ∀ w : v.Extension B, w.1.adicCompletion L :=
…
```
abbrev IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChange The canonical ring homomorphism L ⊗_K K_v → ∏_{w|v} L_w as an L-algebra map line 259 source
Source documentation
The canonical ring homomorphism L ⊗_K K_v → ∏_{w|v} L_w as an L-algebra map.
```
noncomputable abbrev baseChange :
    L ⊗[K] adicCompletion K v →ₐ[L] Π w : v.Extension B, w.1.adicCompletion L :=
…
```
lemma IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChange_tmul_apply line 263 source
abbrev IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight The canonical ring homomorphism L ⊗_K K_v → ∏_{w|v} L_w as an K_v-linear map line 268 source
Source documentation
The canonical ring homomorphism L ⊗_K K_v → ∏_{w|v} L_w as an K_v-linear map.
```
noncomputable abbrev baseChangeRight :
    L ⊗[K] adicCompletion K v →ₐ[adicCompletion K v] Π w : v.Extension B, w.1.adicCompletion L :=
…
```
lemma IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight_surjective The canonical map L ⊗[K] K_v → ∏_{w|v} L_w is surjective line 297 source
Source documentation
The canonical map L ⊗[K] K_v → ∏_{w|v} L_w is surjective.
```
lemma baseChangeRight_surjective [FiniteDimensional K L] :
    Function.Surjective (baseChangeRight K L B v) := by
…
```
Mentions: IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight
instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.(instance at line 316) line 316 source
Source documentation
∏_{w|v} L_w is a finite K_v-module.
```
instance [FiniteDimensional K L] :
    Module.Finite (adicCompletion K v) (Π w : v.Extension B, w.1.adicCompletion L) :=
…
```
instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.(instance at line 321) line 321 source
Source documentation
L_w is a finite K_v-module if w | v.
```
instance [FiniteDimensional K L] (w : v.Extension B) :
    Module.Finite (adicCompletion K v) (adicCompletion L w.1) :=
…
```
instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsModuleTopology L_w has the K_v-module topology line 326 source
Source documentation
L_w has the K_v-module topology.
```
instance instIsModuleTopology [FiniteDimensional K L] (w : v.Extension B) :
    IsModuleTopology (v.adicCompletion K) (w.1.adicCompletion L) := by
…
```

instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsModuleTopologyPi ∏_{w|v} L_w has the K_v-module topology line 335 source

Source documentation

∏_{w|v} L_w has the K_v-module topology.

instance instIsModuleTopologyPi [FiniteDimensional K L] :
    -- the claim that L_w has the module topology.
    IsModuleTopology (v.adicCompletion K) (Π (w : v.Extension B), w.1.adicCompletion L) := by
…

lemma IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight_isOpenQuotientMap tensorAdicCompletionComapLinearMap is continuous, open and surjective line 344 source
Source documentation
tensorAdicCompletionComapLinearMap is continuous, open and surjective. We later show that it's a homeomorphism.
```
lemma baseChangeRight_isOpenQuotientMap [FiniteDimensional K L] :
    IsOpenQuotientMap (baseChangeRight K L B v) := by
…
```
Mentions: IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight
def IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo The canonical B-algebra map B ⊗[A] 𝓞_v → L ⊗[K] K_v line 364 source
Source documentation
The canonical B-algebra map B ⊗[A] 𝓞_v → L ⊗[K] K_v
```
noncomputable def tensorAdicCompletionIntegersTo :
    B ⊗[A] adicCompletionIntegers K v →ₐ[B] L ⊗[K] adicCompletion K v :=
…
```
lemma IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo_tmul line 373 source
lemma IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo_range_subset_closure The image of B ⊗[A] 𝓞_v in L ⊗[K] K_v is contained in the closure of the image of B line 381 source
Source documentation
The image of B ⊗[A] 𝓞_v in L ⊗[K] K_v is contained in the closure of the image of B.
```
lemma tensorAdicCompletionIntegersTo_range_subset_closure [FiniteDimensional K L] :
  (tensorAdicCompletionIntegersTo K L B v).range.carrier ⊆
    closure (algebraMap B (L ⊗[K] adicCompletion K v)).range := by
…
```
Mentions: IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo
lemma IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo_isClopen_range The image of B ⊗[A] 𝓞_v in L ⊗[K] K_v is clopen line 431 source
Source documentation
The image of B ⊗[A] 𝓞_v in L ⊗[K] K_v is clopen.
```
lemma tensorAdicCompletionIntegersTo_isClopen_range
    [IsIntegralClosure B A L] [FiniteDimensional K L] :
    IsClopen (SetLike.coe (tensorAdicCompletionIntegersTo K L B v).range) := by
…
```
Mentions: IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo
lemma IsDedekindDomain.HeightOneSpectrum.range_tensorAdicCompletionIntegersTo_eq_closure_range_algebraMap The image of B ⊗[A] 𝓞_v in L ⊗[K] K_v is the closure of the image of B line 484 source
Source documentation
The image of B ⊗[A] 𝓞_v in L ⊗[K] K_v is the closure of the image of B.
```
lemma range_tensorAdicCompletionIntegersTo_eq_closure_range_algebraMap
    [IsIntegralClosure B A L] [FiniteDimensional K L] :
    Set.range (tensorAdicCompletionIntegersTo K L B v) =
      closure (Set.range (algebraMap B (L ⊗[K] adicCompletion K v))) := by
…
```
Mentions: IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo
lemma IsDedekindDomain.HeightOneSpectrum.pi_adicCompletionIntegers_eq_closure_range_algebraMap The B-subalgebra ∏_{w|v} 𝓞_w of ∏_{w|v} L_w is the closure of the image of B line 499 source
Source documentation
The B-subalgebra ∏_{w|v} 𝓞_w of ∏_{w|v} L_w is the closure of the image of B.
```
lemma pi_adicCompletionIntegers_eq_closure_range_algebraMap :
    (Set.univ.pi (fun (w : Extension B v) ↦ (w.1.adicCompletionIntegers L).carrier)) =
      closure (Set.range (algebraMap B _)) := by
…
```
Mentions: IsDedekindDomain.HeightOneSpectrum.Extension
lemma IsDedekindDomain.HeightOneSpectrum.isClosed_baseChange_image_closure_range_algebraMap The image of B ⊗[A] 𝓞_v (the closure of B) in ∏_w L_w is closed line 510 source
Source documentation
The image of B ⊗[A] 𝓞_v (the closure of B) in ∏_w L_w is closed.
```
lemma isClosed_baseChange_image_closure_range_algebraMap [FiniteDimensional K L] :
    IsClosed ((baseChange K L B v) ''
        closure (Set.range (algebraMap B (L ⊗[K] adicCompletion K v)))) := by
…
```
instance IsDedekindDomain.HeightOneSpectrum.(instance at line 526) line 526 source
theorem IsDedekindDomain.HeightOneSpectrum.range_baseChange_comp_tensorAdicCompletionTo_eq_pi The image of B ⊗[A] 𝓞_v in ∏_w L_w is ∏_w 𝓞_w line 535 source
Source documentation
The image of B ⊗[A] 𝓞_v in ∏_w L_w is ∏_w 𝓞_w.
```
theorem range_baseChange_comp_tensorAdicCompletionTo_eq_pi [FiniteDimensional K L] :
    Set.range (baseChange K L B v ∘ tensorAdicCompletionIntegersTo K L B v) =
    Set.univ.pi (fun w ↦ (w.1.adicCompletionIntegers L).carrier) := by
…
```
Mentions: IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo
def IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionIntegersRingHom The restriction of adicCompletionSemialgHom to a map 𝓞_v → 𝓞_w line 554 source
Source documentation
The restriction of adicCompletionSemialgHom to a map 𝓞_v → 𝓞_w.
```
noncomputable def adicCompletionIntegersRingHom :
    v.adicCompletionIntegers K →+* w.1.adicCompletionIntegers L :=
…
```
instance IsDedekindDomain.HeightOneSpectrum.Extension.(instance at line 560) line 560 source
Source documentation
If w is an extension of v, then 𝓞_w is naturally an 𝓞_v-algebra.
```
noncomputable instance : Algebra (v.adicCompletionIntegers K) (w.1.adicCompletionIntegers L) :=
…
```
lemma IsDedekindDomain.HeightOneSpectrum.Extension.integer_algebraMap_apply line 563 source
instance IsDedekindDomain.HeightOneSpectrum.Extension.(instance at line 569) line 569 source
Source documentation
If w is an extension of v, then L_w is naturally an 𝓞_v-algebra.
```
noncomputable instance : Algebra (v.adicCompletionIntegers K) (w.1.adicCompletion L) :=
…
```
instance IsDedekindDomain.HeightOneSpectrum.(instance at line 575) line 575 source
instance IsDedekindDomain.HeightOneSpectrum.(instance at line 582) line 582 source
def IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersToPiRight The O_v-linear map from B ⊗[A] 𝓞ᵥ to Π v ∣ w, L_w line 587 source
Source documentation
The O_v-linear map from B ⊗[A] 𝓞ᵥ to Π v ∣ w, L_w

depends on sorry (Lean reported 1 error(s) in this file) what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, IsDedekindDomain.HeightOneSpectrum, AlgHom, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, TensorProduct, IsDedekindDomain.HeightOneSpectrum.Extension, Eq, IsDedekindDomain.HeightOneSpectrum.under, TensorProduct.RightActions.instAlgebra_fLT
Proof uses: AlgHom.comp, AlgHom.restrictScalars, IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight, AlgHom.changeScalars, IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo
63 instances, coercions and auxiliary constants left out.
```
noncomputable def tensorAdicCompletionIntegersToPiRight :
    B ⊗[A] v.adicCompletionIntegers K →ₐ[v.adicCompletionIntegers K]
        Π w : v.Extension B, w.1.adicCompletion L :=
…
```
def IsDedekindDomain.HeightOneSpectrum.Extension.tensorAdicCompletionIntegersToAdicCompletion The map B ⊗ 𝓞_v → L_w for w an extension of v given by the algebra maps line 599 source
Source documentation
The map B ⊗ 𝓞_v → L_w for w an extension of v given by the algebra maps.

depends on sorry (Lean reported 1 error(s) in this file) what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.Extension, AlgHom, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, TensorProduct, Eq, IsDedekindDomain.HeightOneSpectrum.under, TensorProduct.RightActions.instAlgebra_fLT
Proof uses: AlgHom.comp, Pi.evalAlgHom, IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersToPiRight
48 instances, coercions and auxiliary constants left out.
```
noncomputable def tensorAdicCompletionIntegersToAdicCompletion :
    B ⊗[A] (adicCompletionIntegers K v) →ₐ[adicCompletionIntegers K v] adicCompletion L w.1 :=
…
```
lemma IsDedekindDomain.HeightOneSpectrum.Extension.tensorAdicCompletionIntegersToAdicCompletion_range_eq_integers The range of adicCompletionIntegers.tensorToAdicCompletion is 𝓞_w line 605 source
Source documentation
The range of adicCompletionIntegers.tensorToAdicCompletion is 𝓞_w.

depends on sorry (Lean reported 1 error(s) in this file) what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.Extension, FiniteDimensional, Eq, Set, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.HeightOneSpectrum.under, Set.range, TensorProduct, Subtype, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers and 3 more
Proof uses: Set.ext, Function.comp, IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChange, IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo, Set.pi, Set.univ, Subsemigroup.carrier, Submonoid.toSubsemigroup, Subsemiring.toSubmonoid, Subring.toSubsemiring, ValuationSubring.toSubring, IsDedekindDomain.HeightOneSpectrum.range_baseChange_comp_tensorAdicCompletionTo_eq_pi, Iff.intro, Iff.mp, Eq.mp, Iff, congrArg, propext, Set.ext_iff, Set.mem_range_self and 18 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma tensorAdicCompletionIntegersToAdicCompletion_range_eq_integers [FiniteDimensional K L] :
    Set.range (w.tensorAdicCompletionIntegersToAdicCompletion K L B v) =
      adicCompletionIntegers L w.1 := by
…
```
instance IsDedekindDomain.HeightOneSpectrum.Extension.(instance at line 637) line 637 source
Source documentation
𝓞_w is finite over 𝓞_v.
```
noncomputable instance (priority := 1001) [Module.Finite A B] [FiniteDimensional K L] :
…
```
lemma IsDedekindDomain.HeightOneSpectrum.adicCompletion._root_.WithZero.ofAdd_neg_ofNat_pow line 667 source
lemma IsDedekindDomain.HeightOneSpectrum.adicCompletion.liesOver_completionIdeal The maximal ideal of 𝒪_w lies over the maximal ideal of 𝒪_v line 672 source
Source documentation
The maximal ideal of 𝒪_w lies over the maximal ideal of 𝒪_v.
```
lemma liesOver_completionIdeal :
    (w.1.completionIdeal L).LiesOver (v.completionIdeal K) where
…
```
theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ramificationIdx_eq_ramificationIdx The local ramification index of L_w/K_v equals the global ramification index of w/v line 682 source
Source documentation
The local ramification index of L_w/K_v equals the global ramification index of w/v.
```
theorem ramificationIdx_eq_ramificationIdx :
    (w.1.completionIdeal L).ramificationIdx (v.adicCompletionIntegers K) =
      w.1.asIdeal.ramificationIdx A := by
…
```
theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.inertiaDeg_eq_inertiaDeg The local inertia degree of L_w/K_v equals the global inertia degree of w/v line 717 source
Source documentation
The local inertia degree of L_w/K_v equals the global inertia degree of w/v.
```
theorem inertiaDeg_eq_inertiaDeg :
    w.1.asIdeal.inertiaDeg A =
      Ideal.inertiaDeg (w.1.completionIdeal L) (v.adicCompletionIntegers K) :=
…
```
theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ramificationIdx_mul_inertiaDeg_eq_finrank Documented declaration: ramificationIdx_mul_inertiaDeg_eq_finrank line 749 source
Source comment
We use Ideal.ramificationIdx_mul_inertiaDeg_eq_finrank_of_isLocalRing here to show this, but we could make use of the more general results in BGR: - in general e * f <= degree (Prop 3.1.3.2) - equality holds for L/K if L is K-cartesian (Prop 3.6.2.4) - so for example if K is complete and discretely-valued (Cor 2.4.3.11).

depends on sorry (Lean reported 1 error(s) in this file) what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.Extension, FiniteDimensional, Module.Finite, Eq, Nat, HMul.hMul, Ideal.ramificationIdx, IsDedekindDomain.HeightOneSpectrum.asIdeal, IsDedekindDomain.HeightOneSpectrum.under, Ideal.inertiaDeg, Module.finrank, IsDedekindDomain.HeightOneSpectrum.adicCompletion
Proof uses: Subtype, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, IsScalarTower.of_algebraMap_smul, rfl, HSMul.hSMul, RingHom, Algebra.algebraMap, FaithfulSMul, FaithfulSMul.of_field_isFractionRing, Eq.mpr, id, congrArg, IsFractionRing.finrank_eq, IsLocalRing.maximalIdeal, Eq.symm, Ideal.ramificationIdx_mul_inertiaDeg_eq_finrank_of_isLocalRing, IsDedekindDomain.HeightOneSpectrum.completionIdeal, IsDedekindDomain.HeightOneSpectrum.completionIdeal_ne_bot and 3 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem ramificationIdx_mul_inertiaDeg_eq_finrank [FiniteDimensional K L] [Module.Finite A B] :
    w.1.asIdeal.ramificationIdx A * w.1.asIdeal.inertiaDeg A =
      Module.finrank (adicCompletion K v) (adicCompletion L w.1) := by
…
```
lemma IsDedekindDomain.HeightOneSpectrum.adicCompletion.finrank_tensorProduct_adicCompletion_eq_finrank_pi_adicCompletion L ⊗[K] K_v and ∏_{w|v} L_w have equal dimensions line 772 source
Source documentation
L ⊗[K] K_v and ∏_{w|v} L_w have equal dimensions

depends on sorry (Lean reported 1 error(s) in this file) what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, FiniteDimensional, Module.Finite, IsDedekindDomain.HeightOneSpectrum, Eq, Nat, Module.finrank, IsDedekindDomain.HeightOneSpectrum.adicCompletion, TensorProduct, TensorProduct.RightActions.instModule_fLT, IsDedekindDomain.HeightOneSpectrum.Extension, IsDedekindDomain.HeightOneSpectrum.under, Subtype
Proof uses: Trans.trans, Finset.sum, Finset.univ, IsDedekindDomain.HeightOneSpectrum.Extension.fintype, HMul.hMul, Ideal.ramificationIdx, IsDedekindDomain.HeightOneSpectrum.asIdeal, Ideal.inertiaDeg, rfl, Eq.mpr, id, congrArg, TensorProduct.finrank_rightAlgebra, Eq.refl, Ideal.sum_ramification_inertia_extensions, Finset.sum_congr, Finset, Membership.mem, IsDedekindDomain.HeightOneSpectrum.adicCompletion.ramificationIdx_mul_inertiaDeg_eq_finrank, Module.finrank_pi_fintype
67 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma finrank_tensorProduct_adicCompletion_eq_finrank_pi_adicCompletion :
    Module.finrank (adicCompletion K v) (L ⊗[K] adicCompletion K v) =
      Module.finrank (adicCompletion K v) ((w : Extension B v) → adicCompletion L w.val) :=
…
```
Mentions: IsDedekindDomain.HeightOneSpectrum.Extension
theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChange_bijective The canonical map L ⊗[K] K_v → ∏_{w|v} L_w is bijective line 787 source
Source documentation
The canonical map L ⊗[K] K_v → ∏_{w|v} L_w is bijective.

depends on sorry (Lean reported 1 error(s) in this file) what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, FiniteDimensional, Module.Finite, IsDedekindDomain.HeightOneSpectrum, Function.Bijective, TensorProduct, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.HeightOneSpectrum.Extension, Eq, IsDedekindDomain.HeightOneSpectrum.under, AlgHom, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChange
Proof uses: id, Function.Surjective, TensorProduct.RightActions.instAlgebra_fLT, IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight, IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight_surjective, And.intro, Function.Injective, Nat, Module.finrank, TensorProduct.RightActions.instModule_fLT, IsDedekindDomain.HeightOneSpectrum.adicCompletion.finrank_tensorProduct_adicCompletion_eq_finrank_pi_adicCompletion, Eq.mpr, LinearMap, RingHom.id, AlgHom.toLinearMap, congrArg, Eq.symm, AlgHom.coe_toLinearMap, propext, LinearMap.injective_iff_surjective_of_finrank_eq_finrank and 1 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem baseChange_bijective : Function.Bijective (baseChange K L B v) := by
…
```
Mentions: IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChange
def IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeAlgEquiv The L-algebra isomorphism L ⊗[K] K_v ≅ ∏_{w|v} L_w line 795 source
Source documentation
The L-algebra isomorphism L ⊗[K] K_v ≅ ∏_{w|v} L_w.

depends on sorry (Lean reported 1 error(s) in this file) what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, FiniteDimensional, Module.Finite, IsDedekindDomain.HeightOneSpectrum, AlgEquiv, TensorProduct, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.HeightOneSpectrum.Extension, Eq, IsDedekindDomain.HeightOneSpectrum.under, Subtype
Proof uses: AlgEquiv.ofBijective, IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChange, IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChange_bijective
42 instances, coercions and auxiliary constants left out.
```
noncomputable def baseChangeAlgEquiv :
    L ⊗[K] v.adicCompletion K ≃ₐ[L] Π w : v.Extension B, w.1.adicCompletion L :=
…
```
def IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeContinuousAlgEquiv The continuous L-algebra isomorphism L ⊗[K] K_v ≅ ∏_{w|v} L_w line 802 source
Source documentation
The continuous L-algebra isomorphism L ⊗[K] K_v ≅ ∏_{w|v} L_w.

depends on sorry (Lean reported 1 error(s) in this file) what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, FiniteDimensional, Module.Finite, IsDedekindDomain.HeightOneSpectrum, ContinuousAlgEquiv, TensorProduct, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.HeightOneSpectrum.Extension, Eq, IsDedekindDomain.HeightOneSpectrum.under, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT
Proof uses: IsBiscalar, TensorProduct.RightActions.instModule_fLT, AlgHom, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeAlgEquiv, IsModuleTopology.continuousAlgEquivOfIsBiscalar, TensorProduct.RightActions.instAlgebra_fLT
62 instances, coercions and auxiliary constants left out.
```
noncomputable def baseChangeContinuousAlgEquiv :
    L ⊗[K] v.adicCompletion K ≃A[L] Π w : v.Extension B, w.1.adicCompletion L :=
…
```
def IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquiv The B-module isomorphism B ⊗[A] K_v ≅ ∏_{w|v} L_w line 810 source
Source documentation
The B-module isomorphism B ⊗[A] K_v ≅ ∏_{w|v} L_w.

depends on sorry (Lean reported 1 error(s) in this file) what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, FiniteDimensional, Module.Finite, IsDedekindDomain.HeightOneSpectrum, LinearEquiv, RingHom.id, TensorProduct, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.HeightOneSpectrum.Extension, Eq, IsDedekindDomain.HeightOneSpectrum.under, Subtype
Proof uses: LinearEquiv.trans, LinearEquiv.symm, IsDedekindDomain.linearEquivTensorProductModuleLeft, LinearEquiv.restrictScalars, IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeAlgEquiv
61 instances, coercions and auxiliary constants left out.
```
noncomputable def integerBaseChangeLinearEquiv :
    B ⊗[A] v.adicCompletion K ≃ₗ[B] ∀ w : v.Extension B, w.1.adicCompletion L :=
…
```
lemma IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquiv_tmul_apply line 816 source
depends on sorry (Lean reported 1 error(s) in this file) what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, FiniteDimensional, Module.Finite, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.Extension, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, IsDedekindDomain.HeightOneSpectrum.under, LinearEquiv, RingHom.id, TensorProduct, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquiv, TensorProduct.tmul and 3 more
Proof uses: Eq.mpr, LinearEquiv.trans, LinearEquiv.symm, IsDedekindDomain.linearEquivTensorProductModuleLeft, LinearEquiv.restrictScalars, IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeAlgEquiv, id, congrArg, IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquiv.eq_1, LinearEquiv.trans_apply, IsDedekindDomain.linearEquivTensorProductModuleLeft_symm_tmul, Eq.refl
83 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerSubmodule 𝓞_v as an A-submodule of K_v line 824 source
Source documentation
𝓞_v as an A-submodule of K_v.
```
noncomputable def integerSubmodule (v : HeightOneSpectrum A) : Submodule A (adicCompletion K v) :=
…
```
def IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.tensorCoe The canonical B-linear map B ⊗[A] 𝓞_v → B ⊗[A] K_v line 837 source
Source documentation
The canonical B-linear map B ⊗[A] 𝓞_v → B ⊗[A] K_v.
```
noncomputable def tensorCoe : B ⊗[A] v.adicCompletionIntegers K →ₗ[B] B ⊗[A] v.adicCompletion K :=
…
```
lemma IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.tensorCoe_tmul line 843 source
theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquiv_bijOn line 854 source
depends on sorry (Lean reported 1 error(s) in this file) what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, FiniteDimensional, Module.Finite, IsDedekindDomain.HeightOneSpectrum, Set.BijOn, TensorProduct, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.HeightOneSpectrum.Extension, Eq, IsDedekindDomain.HeightOneSpectrum.under, LinearEquiv, RingHom.id, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquiv and 10 more
Proof uses: Set, Set.image, LinearMap.range, Submodule.restrictScalars, Eq.trans, Function.comp, AlgHom, IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChange, IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo, Set.pi, Subsemigroup.carrier, Submonoid.toSubsemigroup, Subsemiring.toSubmonoid, Subring.toSubsemiring, ValuationSubring.toSubring, Eq.mpr, id, congrArg, LinearMap.coe_range, Eq.symm and 45 more
142 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.