## Stream: FLT-regular

### Topic: Power basis

#### Riccardo Brasca (Feb 12 2022 at 12:14):

I've added src/ready_for_mathlib/discriminant/power_basis.lean that contains some statements about power_basis that we need. I will not have time to work on it today, but if someone wants to play with it I don't have any objections.

It has the minimal assumptions to write the statements, but in such generality it is probably false, feel free to add any reasonable assumption you want (the main example is A = ℤ, R = ℚ and S = cyclotomic_field p ℚ).

#### Riccardo Brasca (Feb 23 2022 at 16:23):

After some days working on the LTE I am back to this. Does anyone see a quick way of constructing the following?

def of_mem_adjon {x : L} {B : power_basis K L} (hs : B.gen ∈ adjoin K ({x} : set L)) :
power_basis K L :=


#### Anne Baanen (Feb 23 2022 at 16:24):

I assume you want of_mem_adjoin.gen = x?

#### Riccardo Brasca (Feb 23 2022 at 16:27):

Ahah, yes, of course :D

#### Anne Baanen (Feb 23 2022 at 16:28):

Otherwise I would just get away with returning B :)

#### Anne Baanen (Feb 23 2022 at 16:41):

Ok, I'll try and see if I can prove it

#### Eric Rodriguez (Feb 23 2022 at 16:42):

Isn't this basically the lemma we discussed earlier Anne? Except with the assumption slightly different

#### Eric Rodriguez (Feb 23 2022 at 16:42):

I thought we could get around it here riccardo, using the power basis for primitive roots - what do you need it for?

#### Eric Rodriguez (Feb 23 2022 at 16:43):

I was hoping to eventually prove it in the annihilating polynomial version (someone is just PRing that into mathlib right now)

#### Riccardo Brasca (Feb 23 2022 at 16:47):

I need the power basis given by ζ - 1...

#### Riccardo Brasca (Feb 23 2022 at 16:47):

It's nothing especially difficult, my question is only if this is more or less already done somewhere

#### Riccardo Brasca (Feb 23 2022 at 17:00):

import ring_theory.power_basis
import ring_theory.algebraic

universes u v z

variables {R : Type z} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S]
variables {K : Type u} {L : Type v} [field K] [field L] [algebra K L] (B : power_basis K L)

open algebra polynomial

namespace power_basis

lemma adjoin_gen_eq_top (B : power_basis R S) : adjoin R ({B.gen} : set S) = ⊤ :=
begin
rw [← to_submodule_eq_top, _root_.eq_top_iff, ← B.basis.span_eq, submodule.span_le],
rintros x ⟨i, rfl⟩,
rw [B.basis_eq_pow i],
exact subalgebra.pow_mem _ (subset_adjoin (set.mem_singleton _)) _,
end

lemma adjoin_eq_top_of_gen_mem (B : power_basis R S) {x : S} (hx : B.gen ∈ adjoin R ({x} : set S)) :
adjoin R ({x} : set S) = ⊤ :=
begin
simp [hx],
end

/-- The power basis given by x if B.gen ∈ adjoin K {x}. -/
noncomputable def of_mem_adjon {x : L} (hx : B.gen ∈ adjoin K ({x} : set L)) :
power_basis K L :=
by { letI := B.finite_dimensional, exact (adjoin.power_basis $algebra.is_integral_of_finite K L x).map ((subalgebra.equiv_of_eq _ _$

lemma of_mem_adjon_gen {x : L} (hs : B.gen ∈ adjoin K ({x} : set L)) :
(B.of_mem_adjon hs).gen = x := rfl

end power_basis


#### Anne Baanen (Feb 23 2022 at 17:02):

That was exactly my plan too, got distracted by planning dinner :)

#### Riccardo Brasca (Feb 23 2022 at 17:10):

I find slightly annoying that I had to use both docs#subalgebra.equiv_of_eq and docs#algebra.top_equiv, but I guess this is life.

#### Riccardo Brasca (Feb 12 2022 at 12:14):

I've added src/ready_for_mathlib/discriminant/power_basis.lean that contains some statements about power_basis that we need. I will not have time to work on it today, but if someone wants to play with it I don't have any objections.

It has the minimal assumptions to write the statements, but in such generality it is probably false, feel free to add any reasonable assumption you want (the main example is A = ℤ, R = ℚ and S = cyclotomic_field p ℚ).

#### Riccardo Brasca (Feb 23 2022 at 16:23):

After some days working on the LTE I am back to this. Does anyone see a quick way of constructing the following?

def of_mem_adjon {x : L} {B : power_basis K L} (hs : B.gen ∈ adjoin K ({x} : set L)) :
power_basis K L :=


#### Anne Baanen (Feb 23 2022 at 16:24):

I assume you want of_mem_adjoin.gen = x?

#### Riccardo Brasca (Feb 23 2022 at 16:27):

Ahah, yes, of course :D

#### Anne Baanen (Feb 23 2022 at 16:28):

Otherwise I would just get away with returning B :)

#### Anne Baanen (Feb 23 2022 at 16:41):

Ok, I'll try and see if I can prove it

#### Eric Rodriguez (Feb 23 2022 at 16:42):

Isn't this basically the lemma we discussed earlier Anne? Except with the assumption slightly different

#### Eric Rodriguez (Feb 23 2022 at 16:42):

I thought we could get around it here riccardo, using the power basis for primitive roots - what do you need it for?

#### Eric Rodriguez (Feb 23 2022 at 16:43):

I was hoping to eventually prove it in the annihilating polynomial version (someone is just PRing that into mathlib right now)

#### Riccardo Brasca (Feb 23 2022 at 16:47):

I need the power basis given by ζ - 1...

#### Riccardo Brasca (Feb 23 2022 at 16:47):

It's nothing especially difficult, my question is only if this is more or less already done somewhere

#### Riccardo Brasca (Feb 23 2022 at 17:00):

import ring_theory.power_basis
import ring_theory.algebraic

universes u v z

variables {R : Type z} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S]
variables {K : Type u} {L : Type v} [field K] [field L] [algebra K L] (B : power_basis K L)

open algebra polynomial

namespace power_basis

lemma adjoin_gen_eq_top (B : power_basis R S) : adjoin R ({B.gen} : set S) = ⊤ :=
begin
rw [← to_submodule_eq_top, _root_.eq_top_iff, ← B.basis.span_eq, submodule.span_le],
rintros x ⟨i, rfl⟩,
rw [B.basis_eq_pow i],
exact subalgebra.pow_mem _ (subset_adjoin (set.mem_singleton _)) _,
end

lemma adjoin_eq_top_of_gen_mem (B : power_basis R S) {x : S} (hx : B.gen ∈ adjoin R ({x} : set S)) :
adjoin R ({x} : set S) = ⊤ :=
begin
simp [hx],
end

/-- The power basis given by x if B.gen ∈ adjoin K {x}. -/
noncomputable def of_mem_adjon {x : L} (hx : B.gen ∈ adjoin K ({x} : set L)) :
power_basis K L :=
by { letI := B.finite_dimensional, exact (adjoin.power_basis $algebra.is_integral_of_finite K L x).map ((subalgebra.equiv_of_eq _ _$

lemma of_mem_adjon_gen {x : L} (hs : B.gen ∈ adjoin K ({x} : set L)) :
(B.of_mem_adjon hs).gen = x := rfl

end power_basis


#### Anne Baanen (Feb 23 2022 at 17:02):

That was exactly my plan too, got distracted by planning dinner :)

#### Riccardo Brasca (Feb 23 2022 at 17:10):

I find slightly annoying that I had to use both docs#subalgebra.equiv_of_eq and docs#algebra.top_equiv, but I guess this is life.

Last updated: Dec 20 2023 at 11:08 UTC