Skip to content

Instantly share code, notes, and snippets.

@alexjbest

alexjbest/nf.lean

Last active Aug 2, 2019
Embed
What would you like to do?
Number fields in lean?
import data.rat.basic
import data.int.basic
import data.nat.basic
import algebra.field
import linear_algebra.finsupp
import ring_theory.polynomial
import ring_theory.algebra
import ring_theory.adjoin_root
import ring_theory.ideals
import algebra.module
import algebra.char_zero
import linear_algebra.finite_dimensional
import tactic.tidy
import tactic.library_search
instance rat_algebra.vector_space {K : Type*} [ring K] [algebra ℚ K] :
vector_space ℚ K := by apply_instance
instance char_zero.rat_algebra (K : Type*) [discrete_field K] [char_zero K] : algebra ℚ K :=
{ smul := λ q r, q * r,
one_smul := λ x, begin simp only [rat.cast_one], exact one_mul _, end,
mul_smul := λ x y b, begin simp only [rat.cast_mul], exact mul_assoc _ _ _ end,
smul_add := λ x y b, begin simp only, exact mul_add _ _ _ end,
smul_zero := λ x, begin simp only, exact mul_zero _ end,
add_smul := λ x y b, begin simp only [rat.cast_add], exact add_mul _ _ _ end,
zero_smul := λ x, begin simp only [rat.cast_zero], exact zero_mul _ end,
to_fun := rat.cast,
hom := { map_one := rat.cast_one,
map_mul := rat.cast_mul,
map_add := rat.cast_add },
commutes' := λ x y, mul_comm y (rat.cast x),
smul_def' := λ x y, rfl }
class number_field (K : Type*) extends discrete_field K :=
(char_zero : char_zero K)
(fin_dim : finite_dimensional ℚ K)
def real_embs (K : Type*) [number_field K] := { f : K → ℝ // is_field_hom f}
theorem field_noeth (K : Type) [discrete_field K] : finite_dimensional K K :=
begin
apply finite_dimensional.of_fg,
use {1},
unfold submodule.span,
simp only [submodule.mem_coe, lattice.Inf_eq_top, finset.insert_empty_eq_singleton,
finset.coe_singleton, set.mem_set_of_eq, set.singleton_subset_iff],
intros a h,
ext,
split,
{intro hx, exact set.mem_univ x,},
{
intro hx,
have := a.smul x h,
simp [(•)] at this,
assumption,
},
end
instance : number_field ℚ := {
char_zero := linear_ordered_semiring.to_char_zero,
fin_dim := --begin convert field_noeth ℚ, ext, end,
begin
apply finite_dimensional.of_fg,
use {1},
unfold submodule.span,
simp only [submodule.mem_coe, lattice.Inf_eq_top, finset.insert_empty_eq_singleton,
finset.coe_singleton, set.mem_set_of_eq, set.singleton_subset_iff],
intros a h,
ext,
split,
{intro hx, exact set.mem_univ x,},
{
intro hx,
have := a.smul x h,
simp [(•)] at this,
assumption,
},
end,
..show discrete_field ℚ, by exact rat.discrete_field,
}
variables (f : polynomial ℚ) (h : irreducible f)
include h
lemma nat_coe_eq_nat_rat_coe (m : ℕ) : (m : adjoin_root f) = (m : ℚ) :=
begin
induction m,
{
change 0 = adjoin_root.of (0 : ℚ),
simpa [adjoin_root.of],
},
{
simp only [add_comm, nat.cast_succ],
rw [adjoin_root.is_ring_hom.map_add, adjoin_root.is_ring_hom.map_one, m_ih],
}
end
instance : char_zero (adjoin_root f) := { cast_inj := λ m n,
begin split,
{
intro h1,
rw nat_coe_eq_nat_rat_coe f h m at h1,
rw nat_coe_eq_nat_rat_coe f h n at h1,
unfold_coes at h1,
have := (@adjoin_root.coe_injective ℚ _ f _ ) m n h1,
exact (@nat.cast_injective ℚ _ _ _) m n this,
},
{
intro h,
rwa h,
}
end
}
lemma rat_cast_eq_coe_adjoin (a : ℚ) : (rat.cast a : adjoin_root f) = a :=
eq.symm $ rat.eq_cast (@adjoin_root.of _ _ _ f) (rfl)
(@adjoin_root.is_ring_hom _ _ _ f).map_add
(@adjoin_root.is_ring_hom _ _ _ f).map_mul a
instance adjoin_root.is_add_group_hom : is_add_group_hom (@adjoin_root.mk _ _ _ f) :=
by apply_instance
noncomputable instance : number_field (adjoin_root f) := {
char_zero := _,
fin_dim :=
begin
apply finite_dimensional.of_fg,
unfold submodule.fg,
let X := (@adjoin_root.root _ _ _ f),
let d := polynomial.degree f,
let dnat := polynomial.nat_degree f,
use (finset.image (λ i, X^i) (finset.range dnat)),
simp only [finset.coe_image],
ext g,
split,
{
intro hx,
simp only [submodule.mem_top],
},
{
simp only [⊤, forall_prop_of_true, submodule.mem_top],
--induction x using quotient.induction_on' <- doesn't do the same thing!?
apply quotient.induction_on' g,
intro x,
have : quotient.mk' x = ideal.quotient.mk (ideal.span {f}) x := rfl,
rw this,
have := euclidean_domain.div_add_mod x f,
conv_lhs
begin
congr,
rw ← this,
end,
have : ideal.quotient.mk (ideal.span {f}) f = 0 := adjoin_root.mk_self,
simp only [add_comm, ideal.quotient.mk_mul, ideal.quotient.mk_add, this, zero_mul, add_zero],
-- TODO why doesn't simp do `this` for me?
let mo := x % f,
have modeg: polynomial.degree mo < d :=
euclidean_domain.mod_lt _ (ne_zero_of_irreducible h),
rw finsupp.mem_span_iff_total,
use [mo],
simp only [exists_prop],
split,
{
rw finsupp.mem_supported,
have := polynomial.degree_eq_nat_degree (ne_zero_of_irreducible h),
unfold_coes,
change polynomial.degree mo < polynomial.degree f at modeg,
rw [this] at modeg,
have : mo.support ⊆ (finset.range dnat) := begin
rw finset.subset_iff,
intros ll hll,
rw finset.mem_range,
have : ↑ ll ≤ polynomial.degree mo := finset.le_sup hll,
have : ↑ ll < (dnat: with_bot ℕ) := lt_of_le_of_lt this modeg,
exact with_bot.coe_lt_coe.mp this
end,
exact finset.subset_iff.mpr this,
},
{
rw finsupp.total_apply,
rw ← polynomial.sum_C_mul_X_eq (x % f),
rw finsupp.sum,
rw finsupp.sum,
rw is_add_group_hom.finset_sum (ideal.quotient.mk (ideal.span {f})) _ ((x % f).support),
simp only [ideal.quotient.mk_pow, function.comp_app, ideal.quotient.mk_mul],
{
simp [(•)],
unfold_coes,
have : ((λ (a : ℕ), rat.cast ((mo.to_fun : ℕ → ℚ) a) * X ^ a) : ℕ → adjoin_root f)= (λ (x_1 : ℕ),
adjoin_root.mk (polynomial.C (((x % f).to_fun : ℕ → ℚ) x_1)) *
adjoin_root.mk (polynomial.X) ^ x_1) :=
begin
ext,
rw rat_cast_eq_coe_adjoin _ _ (mo.to_fun x_1),
refl,
end,
conv_lhs
begin
congr,
skip,
rw this,
end,
refl,
},
exactI adjoin_root.is_add_group_hom f h,
}
},
end,
..show discrete_field _, by apply_instance,
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment