CyclotomicAdjoin.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The integral algebra and number field generated by roots of unity

Both objects are concrete subobjects of ℂ. The integer algebra includes literally into the rationally generated intermediate field. Integrality is proved from positive power-equals-one witnesses for the generators; finite generation then supplies the finite-dimensional and number-field structures.

abbrev OAI.CirculantHadamard.CyclotomicAdjoin.Ring line 24
Source documentation
The actual integer algebra generated by s.
```
abbrev Ring (s : Set ℂ) : Type := Algebra.adjoin ℤ s
```
abbrev OAI.CirculantHadamard.CyclotomicAdjoin.Field line 27
Source documentation
The actual intermediate field generated over the rationals by s.
```
abbrev Field (s : Set ℂ) : Type := IntermediateField.adjoin ℚ s
```
theorem OAI.CirculantHadamard.CyclotomicAdjoin.root_integral line 31
Source documentation
Each generator's positive power relation is a monic integral relation over both the integers and the rationals.
```
theorem root_integral (R : Type uR) [CommRing R] [Algebra R ℂ] {ζ : ℂ}
    (hζ : ∃ n : ℕ, 0 < n ∧ ζ ^ n = 1) : IsIntegral R ζ := by
…
```
theorem OAI.CirculantHadamard.CyclotomicAdjoin.ring_le_field line 40
Source documentation
Containment of the integer algebra in the rationally generated field, with the latter viewed as an integer subalgebra of ℂ.
```
theorem ring_le_field (s : Set ℂ) :
    Algebra.adjoin ℤ s ≤
      (IntermediateField.adjoin ℚ s).toSubalgebra.restrictScalars ℤ := by
…
```
def OAI.CirculantHadamard.CyclotomicAdjoin.inclusion line 48
Source documentation
The concrete inclusion preserves the underlying complex number.
```
def inclusion (s : Set ℂ) : Ring s →+* Field s where
…
```
Mentions: OAI.CirculantHadamard.CyclotomicAdjoin.Ring, OAI.CirculantHadamard.CyclotomicAdjoin.Field
theorem OAI.CirculantHadamard.CyclotomicAdjoin.inclusion_coe line 55
theorem OAI.CirculantHadamard.CyclotomicAdjoin.inclusion_injective line 58
theorem OAI.CirculantHadamard.CyclotomicAdjoin.integral line 65
Source documentation
Every element of the integer algebra is integral over the integers. Finiteness of the generator set is not needed for this conclusion.
```
theorem integral {s : Set ℂ}
    (hroots : ∀ ζ ∈ s, ∃ n : ℕ, 0 < n ∧ ζ ^ n = 1)
    (z : Ring s) : IsIntegral ℤ z := by
…
```
Mentions: OAI.CirculantHadamard.CyclotomicAdjoin.Ring
theorem OAI.CirculantHadamard.CyclotomicAdjoin.integral_coe line 73
Source documentation
In particular the corresponding actual complex number is integral.
```
theorem integral_coe {s : Set ℂ}
    (hroots : ∀ ζ ∈ s, ∃ n : ℕ, 0 < n ∧ ζ ^ n = 1)
    (z : Ring s) : IsIntegral ℤ (z : ℂ) :=
…
```
Mentions: OAI.CirculantHadamard.CyclotomicAdjoin.Ring
theorem OAI.CirculantHadamard.CyclotomicAdjoin.inclusion_integral line 79
Source documentation
Integrality of the element after its literal inclusion into the field.
```
theorem inclusion_integral {s : Set ℂ}
    (hroots : ∀ ζ ∈ s, ∃ n : ℕ, 0 < n ∧ ζ ^ n = 1)
    (z : Ring s) : IsIntegral ℤ (inclusion s z) :=
…
```
Mentions: OAI.CirculantHadamard.CyclotomicAdjoin.Ring, OAI.CirculantHadamard.CyclotomicAdjoin.inclusion
theorem OAI.CirculantHadamard.CyclotomicAdjoin.finiteDimensional line 86
Source documentation
A finite set of roots of unity generates a finite-dimensional extension of ℚ.
```
theorem finiteDimensional {s : Set ℂ} (hs : s.Finite)
    (hroots : ∀ ζ ∈ s, ∃ n : ℕ, 0 < n ∧ ζ ^ n = 1) :
    FiniteDimensional ℚ (Field s) := by
…
```
Mentions: OAI.CirculantHadamard.CyclotomicAdjoin.Field
theorem OAI.CirculantHadamard.CyclotomicAdjoin.numberField line 96
Source documentation
The number-field structure for the concrete rational adjoin follows from its finite dimension.
```
theorem numberField {s : Set ℂ} (hs : s.Finite)
    (hroots : ∀ ζ ∈ s, ∃ n : ℕ, 0 < n ∧ ζ ^ n = 1) :
    NumberField (Field s) := by
…
```
Mentions: OAI.CirculantHadamard.CyclotomicAdjoin.Field