Hilbert's theorem 92

This file studies systems of relative units in cyclic extensions for the proof of Hilbert's theorem 92.

@[reducible, inline]

abbrev systemOfUnits.IsMaximal {s p : ℕ} {G : Type u_4} [AddCommGroup G] [Module (CyclotomicIntegers p) G] (sys : systemOfUnits p G s) : Prop

A system of units is maximal if the subgroup generated by it has finite index.

Equations

• sys.IsMaximal = (Submodule.span (CyclotomicIntegers p) (Set.range sys.units)).toAddSubgroup.FiniteIndex

theorem systemOfUnits.isMaximal {s : ℕ} (p : ℕ) (hp : Nat.Prime p) (G : Type u_3) [AddCommGroup G] [Module.Finite ℤ G] (hf : Module.finrank ℤ G = s * (p - 1)) [Module (CyclotomicIntegers p) G] (sys : systemOfUnits p G s) : sys.IsMaximal

A full-rank system of units is maximal.

noncomputable def systemOfUnits.index {s : ℕ} (p : ℕ) (G : Type u_3) [AddCommGroup G] [Module (CyclotomicIntegers p) G] (sys : systemOfUnits p G s) : ℕ

The index of the submodule generated by a maximal system of units.

Equations

• systemOfUnits.index p G sys = (Submodule.span (CyclotomicIntegers p) (Set.range sys.units)).toAddSubgroup.index

def systemOfUnits.IsFundamental {s : ℕ} (p : ℕ) (G : Type u_3) [AddCommGroup G] [Module (CyclotomicIntegers p) G] (h : systemOfUnits p G s) : Prop

A system of units is fundamental if it's maximal and the submodule generated by the elements of the system has smallest index.

Equations

• systemOfUnits.IsFundamental p G h = ∃ (_ : h.IsMaximal), ∀ (S : systemOfUnits p G s), S.IsMaximal → systemOfUnits.index p G h ≤ systemOfUnits.index p G S

theorem systemOfUnits.IsFundamental.maximal' {r : ℕ} (p : ℕ) (G : Type u_3) [AddCommGroup G] [Module (CyclotomicIntegers p) G] (S : systemOfUnits p G r) (hs : IsFundamental p G S) (a : systemOfUnits p G r) [a.IsMaximal] : (Submodule.span (CyclotomicIntegers p) (Set.range S.units)).toAddSubgroup.index ≤ (Submodule.span (CyclotomicIntegers p) (Set.range a.units)).toAddSubgroup.index

theorem systemOfUnits.IsFundamental.existence (p : ℕ) (hp : Nat.Prime p) (G : Type u_3) [AddCommGroup G] (s : ℕ) (hf : Module.finrank ℤ G = s * (p - 1)) [Module.Finite ℤ G] [Module.Free ℤ G] [Module (CyclotomicIntegers p) G] : ∃ (S : systemOfUnits p G s), IsFundamental p G S

theorem systemOfUnits.IsFundamental.lemma2 (p : ℕ) (hp : Nat.Prime p) (G : Type u_3) [AddCommGroup G] (s : ℕ) (hf : Module.finrank ℤ G = s * (p - 1)) [Module.Finite ℤ G] [Module (CyclotomicIntegers p) G] (S : systemOfUnits p G s) (hs : IsFundamental p G S) (i : Fin s) (a : Fin s →₀ CyclotomicIntegers p) (ha : a i = 1) (g : G) : (1 - CyclotomicIntegers.zeta p) • g ≠ (Finsupp.linearCombination (CyclotomicIntegers p) S.units) a

theorem systemOfUnits.IsFundamental.corollary (p : ℕ) (hp : Nat.Prime p) (G : Type u_3) [AddCommGroup G] (s : ℕ) (hf : Module.finrank ℤ G = s * (p - 1)) [Module.Finite ℤ G] [Module (CyclotomicIntegers p) G] (S : systemOfUnits p G s) (hs : IsFundamental p G S) (a : Fin s → ℤ) (ha : ∃ (i : Fin s), ¬↑p ∣ a i) (g : G) : (1 - CyclotomicIntegers.zeta p) • g ≠ ∑ i : Fin s, a i • S.units i

def RelativeUnits (k : Type u_4) (K : Type u_5) [Field k] [Field K] [Algebra k K] : Type u_5

Relative units of an extension, modulo units coming from the base field.

Equations

• RelativeUnits k K = ((NumberField.RingOfIntegers K)ˣ ⧸ (Units.map ↑(algebraMap (NumberField.RingOfIntegers k) (NumberField.RingOfIntegers K))).range)

@[instance_reducible]

instance instCommGroupRelativeUnits {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] : CommGroup (RelativeUnits k K)

Equations

• instCommGroupRelativeUnits = id inferInstance

theorem norm_eq_prod_pow_gen {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] [IsGalois k K] [FiniteDimensional k K] (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) (η : K) : (algebraMap k K) ((Algebra.norm k) η) = ∏ i ∈ Finset.range (orderOf σ), (σ ^ i) η

theorem Hilbert92_aux0 (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (h : ℕ) (ν : (NumberField.RingOfIntegers k)ˣ) (hν : IsPrimitiveRoot ((algebraMap (NumberField.RingOfIntegers k) k) ↑ν) (p ^ h)) (H : ∀ (ε : (NumberField.RingOfIntegers K)ˣ), (algebraMap k K) ((algebraMap (NumberField.RingOfIntegers k) k) ↑ν) ^ p ^ (h - 1) ≠ (algebraMap (NumberField.RingOfIntegers K) K) ↑ε / σ ((algebraMap (NumberField.RingOfIntegers K) K) ↑ε)) : ∃ (η : (NumberField.RingOfIntegers K)ˣ), (Algebra.norm k) ((algebraMap (NumberField.RingOfIntegers K) K) ↑η) = 1 ∧ ∀ (ε : (NumberField.RingOfIntegers K)ˣ), (algebraMap (NumberField.RingOfIntegers K) K) ↑η ≠ (algebraMap (NumberField.RingOfIntegers K) K) ↑ε / σ ((algebraMap (NumberField.RingOfIntegers K) K) ↑ε)

noncomputable def relativeUnitsMap {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] [NumberField K] [NumberField k] (σ : K →ₐ[k] K) : RelativeUnits k K →* RelativeUnits k K

The map on relative units induced by an algebra endomorphism of the extension.

Equations

• One or more equations did not get rendered due to their size.

theorem relativeUnitsMap_mk {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] [NumberField K] [NumberField k] (σ : K →ₐ[k] K) (x : (NumberField.RingOfIntegers K)ˣ) : (relativeUnitsMap σ) ↑x = ↑((Units.map ↑((galRestrictHom (NumberField.RingOfIntegers k) k K (NumberField.RingOfIntegers K)) σ)) x)

@[simp]

theorem relativeUnitsMap_one {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] [NumberField K] [NumberField k] (x : RelativeUnits k K) : (relativeUnitsMap 1) x = x

theorem relativeUnitsMap_mul_apply {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] [NumberField K] [NumberField k] {f g : K →ₐ[k] K} (x : RelativeUnits k K) : (relativeUnitsMap (f * g)) x = (relativeUnitsMap f) ((relativeUnitsMap g) x)

noncomputable def relativeUnitsMapHom {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] [NumberField K] [NumberField k] : (K →ₐ[k] K) →* Monoid.End (RelativeUnits k K)

The monoid homomorphism from algebra endomorphisms to endomorphisms of relative units.

Equations

• relativeUnitsMapHom = { toFun := relativeUnitsMap, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem relativeUnitsMapHom_apply {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] [NumberField K] [NumberField k] (σ : K →ₐ[k] K) : relativeUnitsMapHom σ = relativeUnitsMap σ

theorem isTors' (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) [NumberField K] [NumberField k] [IsGalois k K] : Module.IsTorsionBySet (Polynomial ℤ) (Module.AEval' ((addMonoidEndRingEquivInt (Additive (RelativeUnits k K))) ((MulEquiv.monoidEnd (RelativeUnits k K)) (relativeUnitsMapHom ↑((AlgEquiv.algHomUnitsEquiv k K).symm σ))))) ↑(Ideal.span {Polynomial.cyclotomic p ℤ})

@[reducible, inline]

abbrev relativeUnitsWithGenerator (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] (hp : Nat.Prime p) (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) : Type u_1

Relative units bundled with the generator data used in Hilbert 92.

Equations

• relativeUnitsWithGenerator p hp hKL σ hσ = RelativeUnits k K

@[instance_reducible]

instance instCommGroupRelativeUnitsWithGenerator (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) : CommGroup (relativeUnitsWithGenerator p hp hKL σ hσ)

Equations

• instCommGroupRelativeUnitsWithGenerator p hp hKL σ hσ = id inferInstance

def unitToUHom (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) : Additive (NumberField.RingOfIntegers K)ˣ →+ Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸ AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ))

The additive homomorphism from units to the torsion-free quotient of relative units.

Equations

• One or more equations did not get rendered due to their size.

def unitToU (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) (u : (NumberField.RingOfIntegers K)ˣ) : Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸ AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ))

The image of a unit in the torsion-free quotient of relative units.

Equations

• unitToU p hp hKL σ hσ u = (unitToUHom p hp hKL σ hσ) (Additive.ofMul u)

theorem unit_to_U_one (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) : unitToU p hp hKL σ hσ 1 = 0

theorem unit_to_U_mul (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) (x y : (NumberField.RingOfIntegers K)ˣ) : unitToU p hp hKL σ hσ (x * y) = unitToU p hp hKL σ hσ x + unitToU p hp hKL σ hσ y

theorem unit_to_U_inv (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) (x : (NumberField.RingOfIntegers K)ˣ) : unitToU p hp hKL σ hσ x⁻¹ = -unitToU p hp hKL σ hσ x

theorem unit_to_U_div (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) (x y : (NumberField.RingOfIntegers K)ˣ) : unitToU p hp hKL σ hσ (x / y) = unitToU p hp hKL σ hσ x - unitToU p hp hKL σ hσ y

theorem unit_to_U_prod (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) {ι : Type u_4} (s : Finset ι) (f : ι → (NumberField.RingOfIntegers K)ˣ) : unitToU p hp hKL σ hσ (∏ i ∈ s, f i) = ∑ i ∈ s, unitToU p hp hKL σ hσ (f i)

theorem unit_to_U_pow (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) (x : (NumberField.RingOfIntegers K)ˣ) (n : ℕ) : unitToU p hp hKL σ hσ (x ^ n) = n • unitToU p hp hKL σ hσ x

theorem unit_to_U_zpow (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) (x : (NumberField.RingOfIntegers K)ˣ) (n : ℤ) : unitToU p hp hKL σ hσ (x ^ n) = n • unitToU p hp hKL σ hσ x

theorem unit_to_U_map (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) (x : (NumberField.RingOfIntegers k)ˣ) : unitToU p hp hKL σ hσ ((Units.map ↑(algebraMap (NumberField.RingOfIntegers k) (NumberField.RingOfIntegers K))) x) = 0

theorem exists_pow_smul_eq_and_not_dvd {ι : Type u_4} [Finite ι] (f : ι → ℤ) (hf : f ≠ 0) (p : ℕ) (hp : p ≠ 1) : ∃ (n : ℕ) (f' : ι → ℤ), f = p ^ n • f' ∧ ∃ (i : ι), ¬↑p ∣ f' i

theorem lh_pow_free_aux (p : ℕ) (hp : Nat.Prime p) {M : Type u_4} [CommGroup M] [Module.Finite ℤ (Additive M)] (ν : M) (hk : ∀ (ε : M) (n : ℕ), ε ^ p ^ n = 1 → ∃ (i : ℕ), ν ^ i = ε) (r : ℕ) (hr : Module.finrank ℤ (Additive M) < r) (η : Fin r → Additive M) : ∃ (a : ℤ) (ι : Fin r → ℤ) (i : Fin r), ∑ i : Fin r, ι i • η i = a • Additive.ofMul ν ∧ ¬↑p ∣ ι i

theorem lh_pow_free' (p : ℕ) (hp : Nat.Prime p) {M : Type u_4} [CommGroup M] [Module.Finite ℤ (Additive M)] (ν : M) (hk : ∀ (ε : M) (n : ℕ), ε ^ p ^ n = 1 → ∃ (i : ℕ), ν ^ i = ε) (r : ℕ) (hr : Module.finrank ℤ (Additive M) + 1 < r) (η : Fin r → Additive M) : ∃ (a : ℤ) (ι : Fin r → ℤ) (i : Fin r), ∑ i : Fin r, ι i • η i = (a * ↑p) • Additive.ofMul ν ∧ ¬↑p ∣ ι i ∧ (ν = 1 → ↑i ≠ r - 1)

theorem lh_pow_free (p : ℕ) {k : Type u_2} [Field k] (hp : Nat.Prime p) [NumberField k] (ν : (NumberField.RingOfIntegers k)ˣ) (hk : ∀ (ε : (NumberField.RingOfIntegers k)ˣ) (n : ℕ), ε ^ p ^ n = 1 → ∃ (i : ℕ), ν ^ i = ε) (η : Fin (NumberField.Units.rank k + 2) → Additive (NumberField.RingOfIntegers k)ˣ) : ∃ (a : ℤ) (ι : Fin (NumberField.Units.rank k + 2) → ℤ) (i₀ : Fin (NumberField.Units.rank k + 2)), ∑ i : Fin (NumberField.Units.rank k + 2), ι i • η i = (a * ↑p) • Additive.ofMul ν ∧ ¬↑p ∣ ι i₀ ∧ (ν = 1 → i₀ ≠ Fin.last (NumberField.Units.rank k + 1))

theorem Hilbert92_aux1 (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] (hKL : Module.finrank k K = p) [NumberField k] [NumberField K] (n : ℕ) (H : Fin n → Additive (NumberField.RingOfIntegers K)ˣ) (ν : (NumberField.RingOfIntegers k)ˣ) (a : ℤ) (ι : Fin n → ℤ) (η : Fin n → Additive (NumberField.RingOfIntegers k)ˣ) (ha : ∑ i : Fin n, ι i • η i = (a * ↑p) • Additive.ofMul ν) (hη : ∀ (i : Fin n), (algebraMap (NumberField.RingOfIntegers k) k) ↑(Additive.toMul (η i)) = (Algebra.norm k) ((algebraMap (NumberField.RingOfIntegers K) K) ↑(Additive.toMul (H i)))) : (Algebra.norm k) ((algebraMap (NumberField.RingOfIntegers K) K) ↑(Additive.toMul (∑ i : Fin n, ι i • H i) * (Units.map ↑(algebraMap (NumberField.RingOfIntegers k) (NumberField.RingOfIntegers K))) ν ^ (-a))) = 1

@[instance_reducible]

noncomputable instance relativeUnitsModule (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) [NumberField k] [NumberField K] [IsGalois k K] : Module (CyclotomicIntegers p) (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸ AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))

Equations

• relativeUnitsModule p hp hKL σ hσ = inferInstance

theorem relativeUnitsModule_zeta_smul (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) [NumberField k] [NumberField K] [IsGalois k K] (x : (NumberField.RingOfIntegers K)ˣ) : CyclotomicIntegers.zeta p • unitToU p hp hKL σ hσ x = unitToU p hp hKL σ hσ ((Units.map ↑((galRestrictHom (NumberField.RingOfIntegers k) k K (NumberField.RingOfIntegers K)) ↑σ)) x)

theorem instFiniteIntAdditiveRelativeUnits {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] [NumberField K] : Module.Finite ℤ (Additive (RelativeUnits k K))

theorem instFiniteIntAdditiveRelativeUnitsWithGenerator (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) [NumberField K] : Module.Finite ℤ (Additive (relativeUnitsWithGenerator p hp hKL σ hσ))

theorem instFiniteIntQuotientAdditiveRelativeUnitsWithGeneratorAddSubgroupTorsion (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) [NumberField K] : Module.Finite ℤ (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸ AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))

noncomputable def unitlifts (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) [NumberField k] [NumberField K] [IsGalois k K] (S : systemOfUnits p (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸ AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ))) (NumberField.Units.rank k + 1)) : Fin (NumberField.Units.rank k + 1) → Additive (NumberField.RingOfIntegers K)ˣ

Arbitrary unit representatives lifting a system of units.

Equations

• unitlifts p hp hKL σ hσ S i = Additive.ofMul (Quotient.out (Additive.toMul (Quotient.out (S.units i))))

theorem unitlifts_spec (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) [NumberField k] [NumberField K] [IsGalois k K] (S : systemOfUnits p (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸ AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ))) (NumberField.Units.rank k + 1)) (i : Fin (NumberField.Units.rank k + 1)) : unitToU p hp hKL σ hσ (Additive.toMul (unitlifts p hp hKL σ hσ S i)) = S.units i

theorem u_lemma2 (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) [NumberField k] [NumberField K] [IsGalois k K] (u v : (NumberField.RingOfIntegers K)ˣ) (hu : (algebraMap (NumberField.RingOfIntegers K) K) ↑u = (algebraMap (NumberField.RingOfIntegers K) K) ↑v / σ ((algebraMap (NumberField.RingOfIntegers K) K) ↑v)) : unitToU p hp hKL σ hσ u = (1 - CyclotomicIntegers.zeta p) • unitToU p hp hKL σ hσ v

theorem Hilbert92_aux2 (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) [NumberField k] [NumberField K] [IsGalois k K] (E : (NumberField.RingOfIntegers K)ˣ) (ν : k) (hE : (algebraMap k K) ν = (algebraMap (NumberField.RingOfIntegers K) K) ↑E / σ ((algebraMap (NumberField.RingOfIntegers K) K) ↑E)) (hν : ν ^ p = 1) (hpodd : p ≠ 2) : (algebraMap k K) ((Algebra.norm k) ((algebraMap (NumberField.RingOfIntegers K) K) ↑E)) = (algebraMap (NumberField.RingOfIntegers K) K) ↑E ^ p

theorem NumberField.Units.rank_of_isUnramified {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] [NumberField k] [NumberField K] [IsGalois k K] [IsUnramifiedAtInfinitePlaces k K] : rank K = Module.finrank k K * rank k + Module.finrank k K - 1

theorem finrank_G (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) [NumberField k] [NumberField K] [IsGalois k K] [IsUnramifiedAtInfinitePlaces k K] : Module.finrank ℤ (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸ AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ))) = (NumberField.Units.rank k + 1) * (p - 1)

theorem Hilbert91 (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) [NumberField k] [NumberField K] [IsGalois k K] [IsUnramifiedAtInfinitePlaces k K] : ∃ (S : systemOfUnits p (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸ AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ))) (NumberField.Units.rank k + 1)), systemOfUnits.IsFundamental p (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸ AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ))) S

theorem h_exists' (p : ℕ) {k : Type u_2} [Field k] (hp : Nat.Prime p) [NumberField k] : ∃ (h : ℕ) (ν : (NumberField.RingOfIntegers k)ˣ), IsPrimitiveRoot ((algebraMap (NumberField.RingOfIntegers k) k) ↑ν) (p ^ h) ∧ ∀ (ε : (NumberField.RingOfIntegers k)ˣ) (n : ℕ), ε ^ p ^ n = 1 → ∃ (i : ℕ), ν ^ i = ε

theorem almostHilbert92 (p : ℕ) {K : Type u_1} [Field K] {k : Type u_2} [Field k] (hp : Nat.Prime p) [Algebra k K] (hKL : Module.finrank k K = p) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) [NumberField k] [NumberField K] [IsGalois k K] [IsUnramifiedAtInfinitePlaces k K] (hpodd : p ≠ 2) : ∃ (η : (NumberField.RingOfIntegers K)ˣ), (Algebra.norm k) ((algebraMap (NumberField.RingOfIntegers K) K) ↑η) = 1 ∧ ∀ (ε : (NumberField.RingOfIntegers K)ˣ), (algebraMap (NumberField.RingOfIntegers K) K) ↑η ≠ (algebraMap (NumberField.RingOfIntegers K) K) ↑ε / σ ((algebraMap (NumberField.RingOfIntegers K) K) ↑ε)

theorem Hilbert92 {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] [IsGalois k K] [NumberField k] [NumberField K] (hKL : Nat.Prime (Module.finrank k K)) (hpodd : Module.finrank k K ≠ 2) (σ : Gal(K/k)) (hσ : ∀ (x : Gal(K/k)), x ∈ Subgroup.zpowers σ) : ∃ (η : (NumberField.RingOfIntegers K)ˣ), (Algebra.norm k) ((algebraMap (NumberField.RingOfIntegers K) K) ↑η) = 1 ∧ ∀ (ε : (NumberField.RingOfIntegers K)ˣ), (algebraMap (NumberField.RingOfIntegers K) K) ↑η ≠ (algebraMap (NumberField.RingOfIntegers K) K) ↑ε / σ ((algebraMap (NumberField.RingOfIntegers K) K) ↑ε)