Zulip Chat Archive
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
import ring_theory.adjoin.power_basis
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
rw [_root_.eq_top_iff, ← adjoin_gen_eq_top B],
refine adjoin_le _,
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 _ _ $
adjoin_eq_top_of_gen_mem B hx).trans top_equiv) }
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
import ring_theory.adjoin.power_basis
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
rw [_root_.eq_top_iff, ← adjoin_gen_eq_top B],
refine adjoin_le _,
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 _ _ $
adjoin_eq_top_of_gen_mem B hx).trans top_equiv) }
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