KummerUnramifiedNormalization.lean`

106 declarations, 0 contain sorry, 0 declared as axioms

Étale algebras obtained by adjoining roots of units, and normalization charts for the complete-quadrangle Kummer cover in OpenAI's A Complete Local Domain without a Small Cohen–Macaulay Module, Section 6.

def OAI.KummerEtale.standardPairRootEquiv line 16
Source documentation
A standard etale equation with localization polynomial one is precisely its ordinary root algebra.
```
def standardPairRootEquiv (P : StandardEtalePair R) (hg : P.g = 1) :
    P.Ring ≃ₐ[R] AdjoinRoot P.f := by
…
```

lemma OAI.KummerEtale.unitRoot_bezout line 31

Source documentation

Bezout identity for the unit-root equation, with the precise ring units that make its derivative invertible.

lemma unitRoot_bezout (n : ℕ) (hn : 0 < n) (u v : Rˣ) (hv : (v : R) = (n : R)) :
    derivative (X ^ n - C (u : R)) * (C ((v⁻¹ * u⁻¹ : Rˣ) : R) * X) +
      (X ^ n - C (u : R)) * (- C ((u⁻¹ : Rˣ) : R)) = (1 : R[X]) := by
…

def OAI.KummerEtale.unitRootPair line 50
Source documentation
The explicit standard etale pair for adjoining an n-th root of a unit.
```
def unitRootPair (n : ℕ) (hn : 0 < n) (u v : Rˣ) (hv : (v : R) = (n : R)) :
    StandardEtalePair R where
…
```
theorem OAI.KummerEtale.etale_adjoin_unit_root line 60
Source documentation
Adjoining an n-th root of a unit is etale when n is invertible. These are exactly the hypotheses used in the characteristic-zero cover.
```
theorem etale_adjoin_unit_root (n : ℕ) (hn : 0 < n) (u : R)
    (hu : IsUnit u) (hnunit : IsUnit (n : R)) :
    Algebra.Etale R (AdjoinRoot (X ^ n - C u)) := by
…
```
lemma OAI.EtaleNormal.base_injective line 79
abbrev OAI.EtaleNormal.Generic line 83
lemma OAI.EtaleNormal.inverted_le line 85
instance OAI.EtaleNormal.genericDomain line 90
lemma OAI.EtaleNormal.generic_finite line 96
lemma OAI.EtaleNormal.generic_isField line 103
lemma OAI.EtaleNormal.generic_fractionRing line 109
Source documentation
The generic algebra is the entire fraction field of the etale domain, not just a subring of it.
```
lemma generic_fractionRing : IsFractionRing S (Generic R S) := by
…
```
Mentions: OAI.EtaleNormal.Generic
theorem OAI.EtaleNormal.integrallyClosed line 122
Source documentation
Smooth base change and integral closedness of the base force all integral elements in the generic fraction algebra to lie in the chart.
```
theorem integrallyClosed [IsIntegrallyClosed R] : IsIntegrallyClosed S := by
…
```

theorem OAI.KummerEtale.etale_monic_factor line 154

Source documentation

A monic factor of a unit-root equation itself defines an etale algebra. The Bezout equation is derived, not assumed.

theorem etale_monic_factor (n : ℕ) (hn : 0 < n) (u : Rˣ)
    (hnunit : IsUnit (n : R)) (g : R[X]) (hg : g.Monic)
    (hd : g ∣ X ^ n - C (u : R)) : Algebra.Etale R (AdjoinRoot g) := by
…

theorem OAI.KummerEtale.etale_adjoin_unit_root_in_field line 179
Source documentation
A chosen root inside a field, rather than the whole potentially disconnected root algebra, still provides an etale integral domain cover.
```
theorem etale_adjoin_unit_root_in_field (n : ℕ) (hn : 0 < n) (u : Rˣ)
    (hnunit : IsUnit (n : R)) (x : L) (hx : x ^ n = algebraMap R L (u : R)) :
    Algebra.Etale R (Algebra.adjoin R ({x} : Set L)) := by
…
```

theorem OAI.KummerEtale.exists_domain_unit_root line 195

Source documentation

A finite free étale domain cover with one prescribed root of a unit.

theorem exists_domain_unit_root (n : ℕ) (hn : 0 < n) (hnunit : IsUnit (n : R))
    (u : Rˣ) :
    ∃ (S : Type u) (_ : CommRing S) (_ : IsDomain S) (_ : Algebra R S)
      (_ : Module.Finite R S) (_ : Module.Free R S) (_ : Algebra.Etale R S)
      (_ : IsIntegrallyClosed S),
      ∃ c : Sˣ, (c : S) ^ n = algebraMap R S (u : R) := by
…

theorem OAI.KummerEtale.exists_domain_unit_roots line 225

Source documentation

Simultaneously adjoining the five unit factors can be done by a genuine finite faithfully flat etale integral cover. All roots are actual units.

theorem exists_domain_unit_roots (n : ℕ) (hn : 0 < n) (hnunit : IsUnit (n : R))
    {m : ℕ} (u : Fin m → Rˣ) :
    ∃ (S : Type u) (_ : CommRing S) (_ : IsDomain S) (_ : Algebra R S)
      (_ : Module.Finite R S) (_ : Module.Free R S) (_ : Algebra.Etale R S)
      (_ : IsIntegrallyClosed S),
      (Function.Surjective (PrimeSpectrum.comap (algebraMap R S))) ∧
      ∃ c : Fin m → Sˣ, ∀ i, (c i : S) ^ n = algebraMap R S (u i : R) := by
…

theorem OAI.KummerEtale.finite_unit_roots line 264

Source documentation

The actual finite subalgebra generated by finitely many unit roots is finite free and etale. This concerns the fixed roots inside the original function field, not some unrelated etale cover.

theorem finite_unit_roots (n : ℕ) (hn : 0 < n) (hnunit : IsUnit (n : R))
    (s : Finset L) (hs : ∀ x ∈ s, ∃ u : Rˣ, x ^ n = algebraMap R L (u : R)) :
    Algebra.Etale R (Algebra.adjoin R (s : Set L)) ∧
    Module.Finite R (Algebra.adjoin R (s : Set L)) ∧
    Module.Free R (Algebra.adjoin R (s : Set L)) ∧
    IsIntegrallyClosed (Algebra.adjoin R (s : Set L)) := by
…

theorem OAI.KummerEtale.adjoin_fractionRing line 328
Source documentation
Generators for the original extension over the fraction field give the fraction field of their actual integral subalgebra.
```
theorem adjoin_fractionRing (s : Set L) (hs : Algebra.adjoin K s = ⊤) :
    IsFractionRing (Algebra.adjoin R s) L := by
…
```

theorem OAI.KummerEtale.normalization_unit_roots line 365

Source documentation

The whole normalization off the branch divisor is exactly the root subalgebra and is finite free and etale. All claims concern the SAME field L.

theorem normalization_unit_roots (n : ℕ) (hn : 0 < n) (hnunit : IsUnit (n : R))
    (s : Finset L) (hs : ∀ x ∈ s, ∃ u : Rˣ, x ^ n = algebraMap R L (u : R))
    (hgen : Algebra.adjoin K (s : Set L) = ⊤) :
    integralClosure R L = Algebra.adjoin R (s : Set L) := by
…

def OAI.KummerCover.chosenRoot line 387
lemma OAI.KummerCover.chosenRoot_pow line 390
abbrev OAI.KummerCover.rootField line 394
def OAI.KummerCover.fieldRoot line 397
lemma OAI.KummerCover.fieldRoot_pow line 400
lemma OAI.KummerCover.fieldRoot_generates line 405
instance OAI.KummerCover.finite_rootField line 413
abbrev OAI.KummerLines.R line 424
abbrev OAI.KummerLines.K line 425
def OAI.KummerLines.lineForm line 428
def OAI.KummerLines.point line 429
def OAI.KummerLines.variableIndex line 430
lemma OAI.KummerLines.coefficient_one line 432
lemma OAI.KummerLines.degree_le line 436
lemma OAI.KummerLines.degree_eq line 444
lemma OAI.KummerLines.prime_lineForm line 451
lemma OAI.KummerLines.eval_at_self line 457
lemma OAI.KummerLines.eval_at_other line 460
lemma OAI.KummerLines.pairwise_not_associated line 463
def OAI.KummerLines.radicand line 474
abbrev OAI.KummerLines.L line 475
instance OAI.KummerLines.prime_seven line 476
def OAI.KummerLines.branchProduct line 484
lemma OAI.KummerLines.branchProduct_ne_zero line 485
lemma OAI.KummerLines.branchPowers_le line 487
def OAI.KummerLines.offBranch line 493
Source documentation
The literal affine complement of the five branch lines in A². This subalgebra model keeps the original fraction field C(x,y) definitionally.
```
noncomputable def offBranch : Subalgebra R K :=
…
```
Mentions: OAI.KummerLines.R, OAI.KummerLines.K
abbrev OAI.KummerLines.U line 495
instance OAI.KummerLines.(instance at line 496) line 496
instance OAI.KummerLines.(instance at line 499) line 499
instance OAI.KummerLines.(instance at line 502) line 502
lemma OAI.KummerLines.lineForm_unit line 505
instance OAI.KummerLines.(instance at line 509) line 509
lemma OAI.KummerLines.exponent_unit line 514
def OAI.KummerLines.rootSet line 519
lemma OAI.KummerLines.rootSet_coe line 522
theorem OAI.KummerLines.offBranch_normalization line 529
Source documentation
Over the actual open complement of the arrangement, the normalization is generated as a finite algebra by the original five roots.
```
theorem offBranch_normalization :
    integralClosure U (L p) = Algebra.adjoin U
      (Set.range (KummerCover.fieldRoot (p := p) radicand)) := by
…
```
Mentions: OAI.KummerLines.U, OAI.KummerLines.L, OAI.KummerCover.fieldRoot, OAI.KummerLines.radicand
abbrev OAI.KummerLines.offBranchCover line 542
theorem OAI.KummerLines.offBranchCover_finiteFreeEtale line 546
Source documentation
The actual unramified part of the source cover is finite free etale, not just normal or a finite extension generically.
```
theorem offBranchCover_finiteFreeEtale :
    Module.Finite U (offBranchCover p) ∧ Module.Free U (offBranchCover p) ∧
      Algebra.Etale U (offBranchCover p) := by
…
```
Mentions: OAI.KummerLines.U, OAI.KummerLines.offBranchCover
theorem OAI.KummerLines.offBranchCover_smooth line 565
Source documentation
The normalized cover over the complement of the branch lines is smooth over the complex numbers.
```
theorem offBranchCover_smooth : Algebra.Smooth ℂ (offBranchCover p) := by
…
```
Mentions: OAI.KummerLines.offBranchCover
theorem OAI.KummerLines.offBranchCover_surjective line 574
Source documentation
The finite etale cover is surjective on the actual branch-complement spectrum; no point has been removed from this locus upstairs.
```
theorem offBranchCover_surjective :
    Function.Surjective (PrimeSpectrum.comap (algebraMap U (offBranchCover p))) := by
…
```
Mentions: OAI.KummerLines.U, OAI.KummerLines.offBranchCover
lemma OAI.EtaleRegular.dim_le_of_flat_local line 589
theorem OAI.EtaleRegular.regular_local line 602
theorem OAI.EtaleRegular.regular line 617
Source documentation
Etale coordinate algebras preserve regularity at every prime.
```
theorem regular [IsRegularRing R] [Algebra.Etale R S] : IsRegularRing S := by
…
```
theorem OAI.KummerLines.offBranchCover_regular line 635
def OAI.KummerLines.offBranchRestrictionEquiv line 648
Source documentation
Restricting the normalization of the actual original affine plane to its branch complement gives the same literal finite etale cover. This is an isomorphism of algebras, not only a generic-field identification.
```
def offBranchRestrictionEquiv :
    U ⊗[R] integralClosure R (L p) ≃ₐ[U] offBranchCover p := by
…
```
Mentions: OAI.KummerLines.U, OAI.KummerLines.R, OAI.KummerLines.L, OAI.KummerLines.offBranchCover
theorem OAI.KummerLines.normalization_offBranch_regular line 658
Source documentation
All points of the original normalized cover away from the branch locus are regular. No replacement of the original five-root field or hypothesis of normality/regularity of its normalization occurs.
```
theorem normalization_offBranch_regular :
    IsRegularRing (U ⊗[R] integralClosure R (L p)) := by
…
```
Mentions: OAI.KummerLines.U, OAI.KummerLines.R, OAI.KummerLines.L
lemma OAI.AlgebraicIndependent.of_polynomial_expressions line 677
Source documentation
For a finite family, independence of polynomial expressions in its members forces independence of the original generators. This is the finite transcendence-degree converse needed for the actual ramified Kummer coordinate charts.
```
lemma of_polynomial_expressions {k A ι : Type} [Field k] [CommRing A]
    [IsDomain A] [Algebra k A] [Finite ι] {x y : ι → A}
    (hy : AlgebraicIndependent k y)
    (hmem : ∀ i, y i ∈ Algebra.adjoin k (Set.range x)) :
    AlgebraicIndependent k x := by
…
```

lemma OAI.AlgebraicIndependent.of_powers line 702

Source documentation

Independent powers of finitely many elements give independent roots.

lemma of_powers {k A ι : Type} [Field k] [CommRing A]
    [IsDomain A] [Algebra k A] [Finite ι] {x : ι → A} (n : ι → ℕ)
    (h : AlgebraicIndependent k (fun i => x i ^ n i)) :
    AlgebraicIndependent k x :=
…

abbrev OAI.KummerTriple.root line 720
lemma OAI.KummerTriple.root_pow line 721
lemma OAI.KummerTriple.root_ne_zero line 723
def OAI.KummerTriple.coordinateRoot line 734
Source documentation
Coordinates at the exceptional divisor over the actual triple point (0,0): u is the original root of x, v is root(y)/root(x).
```
def coordinateRoot : Fin 2 → L p := ![root p 0, root p 1 / root p 0]
```
Mentions: OAI.KummerTriple.root
lemma OAI.KummerTriple.coordinateRoot_zero_pow line 735
lemma OAI.KummerTriple.coordinateRoot_one_pow line 737
lemma OAI.KummerTriple.original_root_one line 742
lemma OAI.KummerTriple.coordinateRoot_independent line 746
def OAI.KummerTriple.C line 769
Source documentation
The x-chart of the blowup of the original plane at (0,0). Its coordinates s,t map to x,y/x, and the blowdown is x=s,y=st.
```
def C := MvPolynomial (Fin 2) ℂ
```
instance OAI.KummerTriple.(instance at line 770) line 770
instance OAI.KummerTriple.(instance at line 771) line 771
instance OAI.KummerTriple.(instance at line 772) line 772
instance OAI.KummerTriple.(instance at line 773) line 773
def OAI.KummerTriple.blowdown line 774
instance OAI.KummerTriple.(instance at line 775) line 775
instance OAI.KummerTriple.(instance at line 776) line 776
def OAI.KummerTriple.chartMap line 779
instance OAI.KummerTriple.(instance at line 781) line 781
instance OAI.KummerTriple.(instance at line 782) line 782
lemma OAI.KummerTriple.chartMap_blowdown line 784
instance OAI.KummerTriple.(instance at line 805) line 805
lemma OAI.KummerTriple.chartMap_injective line 808
def OAI.KummerTriple.coordinateAlgebra line 838
Source documentation
The two ramified coordinates form an actual polynomial plane in the original field. No independent auxiliary Kummer field is substituted.
```
def coordinateAlgebra : Subalgebra ℂ (L p) :=
…
```
abbrev OAI.KummerTriple.B line 840
def OAI.KummerTriple.planeEquiv line 841
instance OAI.KummerTriple.(instance at line 842) line 842
instance OAI.KummerTriple.(instance at line 844) line 844
def OAI.KummerTriple.bRoot line 849
def OAI.KummerTriple.planeMap line 851
lemma OAI.KummerTriple.planeMap_comp line 852
instance OAI.KummerTriple.(instance at line 860) line 860
instance OAI.KummerTriple.(instance at line 861) line 861
instance OAI.KummerTriple.(instance at line 863) line 863
lemma OAI.KummerTriple.coordinateRoot_pow line 866
lemma OAI.KummerTriple.coordinateRoot_integral line 873
instance OAI.KummerTriple.(instance at line 880) line 880
instance OAI.KummerTriple.(instance at line 890) line 890
instance OAI.KummerTriple.(instance at line 892) line 892
instance OAI.KummerTriple.(instance at line 893) line 893