From 227d04e7092ba097c16819071099604f41680b01 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Wed, 18 Dec 2024 23:38:50 +0000 Subject: [PATCH] chore: update Frobenius to reflect new mathlib PR. --- FLT/FLT_files.lean | 3 - FLT/MathlibExperiments/Frobenius.lean | 948 --------------------- FLT/MathlibExperiments/Frobenius2.lean | 292 ------- FLT/MathlibExperiments/FrobeniusRiou.lean | 917 -------------------- blueprint/src/chapter/FrobeniusProject.tex | 4 +- 5 files changed, 2 insertions(+), 2162 deletions(-) delete mode 100644 FLT/MathlibExperiments/Frobenius.lean delete mode 100644 FLT/MathlibExperiments/Frobenius2.lean delete mode 100644 FLT/MathlibExperiments/FrobeniusRiou.lean diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean index a46dbe24..787e01b8 100644 --- a/FLT/FLT_files.lean +++ b/FLT/FLT_files.lean @@ -33,9 +33,6 @@ import FLT.Mathlib.Data.ENNReal.Inv import FLT.MathlibExperiments.Coalgebra.Monoid import FLT.MathlibExperiments.Coalgebra.Sweedler import FLT.MathlibExperiments.Coalgebra.TensorProduct -import FLT.MathlibExperiments.Frobenius -import FLT.MathlibExperiments.Frobenius2 -import FLT.MathlibExperiments.FrobeniusRiou import FLT.MathlibExperiments.HopfAlgebra.Basic import FLT.MathlibExperiments.IsCentralSimple import FLT.MathlibExperiments.IsFrobenius diff --git a/FLT/MathlibExperiments/Frobenius.lean b/FLT/MathlibExperiments/Frobenius.lean deleted file mode 100644 index eafc70a9..00000000 --- a/FLT/MathlibExperiments/Frobenius.lean +++ /dev/null @@ -1,948 +0,0 @@ -/- -Copyright (c) 2024 Jou Glasheen. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jou Glasheen --/ -import Mathlib.RingTheory.DedekindDomain.Ideal -import Mathlib.RingTheory.IntegralClosure.IntegralRestrict -import Mathlib.FieldTheory.Cardinality - - -/-! - -# DO NOT FIX THIS FILE IF IT BREAKS. - -It is work in progress. If it breaks just move the #exit up to -just before it breaks. Frobenius elements need a complete refactor -so keeping this code up to date is a waste of time. - -# Frobenius element for finite extensions L / K - -In this file, I : - -· formalize the "direct proof" of the existence of the - Frobenius element for a finite extension of number fields L / K, - as given by J. S. Milne, in footnote '2' on p. 141 of *Algebraic Number Theory*. - -## Main results - -- `gal_action_Ideal'` : the action of the Galois group `L ≃ₐ[K] L` on the prime ideals of `B`, - the ring of integers of `L`. -- `decomposition_subgroup_Ideal'` : the definition of the decomposition subgroup of the - prime ideal `Q ⊂ B` over `K`. -- `exists_generator` : the proof of the second sentence of Milne's proof : - "By the Chinese remainder theorem, - there exists an element `α` of `𝓞 L` such that `α` generates the group `(𝓞 L ⧸ P)ˣ` and - lies in `τ • P` for all `τ ∉ G(P)`", - where `G(P)` denotes the decomposition subgroup of `P` over `K`. - Note that in our file, we rename the non-zero prime ideal `P` as `Q`, - and we use `P` to denote the non-zero prime ideal of `𝓞 K` over which `Q` lies. -- `coeff_lives_in_A` : for `F : B[X]` defined to be the product over linear factors whose - roots are the Galois conjugates of `α`, (i.e., `∏ τ : L ≃ₐ[K] L, - (X - C (galRestrict A K L B τ α))`), - `F` has its coefficients in `A`, where `A` is the ring of integers of - the base field `K`. -- `exists_frobenius` : the existence theorem for Frobenius elements of - finite Galois extension of number fields. - -## Notation - -Note that, to define the `MulAction` of `L ≃ₐ[K] L` on the prime ideals of `𝓞 L : = B`, -we used the restriction map `galRestrict`, defined in the file Mathlib.RingTheory.IntegralClosure.IntegralRestrict. -The definition of `galRestrict` is in terms of an 'AKLB setup'; i.e., where -"`A` is an integrally closed domain; `K` is the fraction ring of `A`; `L` is -a finite (separable) extension of `K`; `B` is the integral closure of -`A` in `L` (Yang & Lutz, 2023, lines 14-15). - -In this file, I use the following notation corresponding to an 'AKLB setup': - -- `A` : the ring of integers of the number field `K`. -- `K` : a number field of finite dimension over `ℚ`. -- `L` : a number field which is a finite extension of `K`. -- `B` : the ring of integers of the number field `L`. -- `P` : a non-zero prime ideal of `A`. -- `Q` : a non-zero prime ideal of `B` which lies over `P`. -- `Ideal' A K L B`: a redefinition of `Ideal B`, which keeps in mind the existence of - the ring `A`; this is because the `MulAction` of `L ≃ₐ[K] L` on `Ideal B` - is defined using `galRestrict`, which requires reference to the scalars `A` - over which the algebraic equivalence `B ≃ₐ[A] B` is defined. -- `f` : the function assigning a representative non-zero prime ideal of `B` to - a coset in the quotient `((L ≃ₐ[K] L) ⧸ decomposition_subgroup_Ideal Q)`, - i.e., an element in the orbit of `Q` under the action of `(L ≃ₐ[K] L)`. -- `p` : a natural prime which is the characteristic of the residue field `(A ⧸ P)`. -- `q` : the cardinality of the residue field `(A ⧸ P)`. We show that `q = p ^ n` for - some `n : ℕ`. -- `ρ` : `α` in Milne's notation. This `ρ` is an element of `B` which generates the group - `(B ⧸ Q)ˣ` and is `0` mod `τ • Q` for any `τ` not in the decomposition subgroup - of `Q` over `K`. -- `α` : local notation for an element `generator : B` which has the properties of `ρ`. -- `F` : local notation for `F' : B[X]`, a polynomial whose roots are exactly the - Galois conjugates of `α`. -- `m` : local notation for `m' : A[x]`, a polynomial constructed such that its lift to - `B` under `algebraMap A B` is equal to `F`. -- `Frob` : local notation for `Frob' : L ≃ₐ[K] L`, an element of the Galois group that - sends `α` to its `q`-th power `mod Q`. -- `γ` : arbitrary element of `B`. We consider the cases `γ ∈ Q`, `γ ∉ Q`, separately. -- `i`: local notation for `i' : ℕ`, such that `γ ≡ α ^ i mod Q`. `i` depends on `γ`. - -## Note : I have changed the previous notation `β → α`, `ν → β`, to conform to Milne's notation. - -## Implementation notes - -This file was written in Prof. Buzzard's 'FLT' repository. - -## References - -See [Milne (2020)] footnote '2' on p. 141 (p. 143 in PDF) - for the proof on which this file is based. - -See [Yang & Lutz (2023)], for the definitions of 'AKLB setup' and `galRestrict`. - -See [Nakagawa, Baanen, & Filippo (2020)], for the definition of - `IsDedekindDomain.exists_forall_sub_mem_ideal`, - the key to proving our theorem `exists_generator`. - -See [Karatarakis (2022)], for the definition of 'decomposition subgroup' in terms of - valuations. - -## Acknowledgements - -The theorems in this file began life as Jou Glasheen's -2023 Formalising Mathematics student project. Kevin thanks -Jou for taking his class and for writing such a great project. -Jou would particularly like to thank two of Kevin's PhD students, Amelia and Jujian, -for "helping me to understand the math proof and to formalize it." - --/ - -set_option linter.unusedSectionVars false - -open Classical - -section FiniteFrobeniusDef - -variable (A K L B : Type*) [CommRing A] [CommRing B] - [Algebra A B] [Field K] [Field L] - [IsDomain A] [IsDomain B] - [Algebra A K] [IsFractionRing A K] - [Algebra B L] [Algebra K L] [Algebra A L] - [IsScalarTower A B L] [IsScalarTower A K L] - [IsIntegralClosure B A L] [FiniteDimensional K L] [IsFractionRing B L] - [IsDedekindDomain A] [IsDedekindDomain B] - -/- -**TODO** - -The below definition of `Ideal'` needs refactoring somehow, but I am not entirely clear -how yet; perhaps when I understand this work better I'll know how to proceed. Right now -it's the ideals of B but under the assumption that we're in some kind of AKLB set-up. - --/ - -/-- re-definition of `Ideal B` in terms of 'AKLB setup'. -/ -@[nolint unusedArguments] abbrev Ideal' (A K L B : Type*) - [Semiring B] [SMul A B] - [SMul A K] [SMul B L] - [SMul K L] [SMul A L] [IsScalarTower A B L] - [IsScalarTower A K L] - := Ideal B - -/- -**TODO** - -I feel like this definition should be broken into three pieces: - -1) Action of `B ≃ₐ[A] B` on `Ideal B` -2) Isomorphism `B ≃ₐ[A] B` = `L ≃ₐ[A] L` if `IsScalarTower A B L` -3) Isomorphism `L ≃ₐ[A] L` = `L ≃ₐ[K] L` if `IsScalarTower A K L`. - - --/ -/-- Action of the Galois group `L ≃ₐ[K] L` on the prime ideals `(Ideal' A K L B)`; -where `(Ideal' A K L B)` denotes `Ideal B` re-defined with respect to the -'AKLB setup'. -/ -noncomputable instance gal_action_Ideal': MulAction (L ≃ₐ[K] L) (Ideal' A K L B) where - smul σ I := Ideal.comap (AlgEquiv.symm (galRestrict A K L B σ)) I - one_smul _ := by - -- `show` unfolds goal into something definitionally equal - show Ideal.comap _ _ = _ - simp only [map_one] - exact Ideal.comap_id _ - mul_smul _ _ := by - intro h - show Ideal.comap _ _ = _ - simp only [map_mul] - rfl - --- The following lemma will be used in `CRTRepresentative` (which is why we --- `@[simp]` it), where it is combined with the assumption (implicit in Milne), --- that `Q` is a *nonzero* prime ideal of `B`. --- it is placed here by convention, as a property of `gal_action_Ideal`. --- Jujian helped me to write this lemma. -@[simp] lemma gal_action_Ideal'.smul_bot (σ : (L ≃ₐ[K] L)) : σ • (⊥ : Ideal' A K L B) = ⊥ := by - apply Ideal.comap_bot_of_injective - exact AlgEquiv.injective (AlgEquiv.symm ((galRestrict A K L B) σ)) - --- I define the decomposition group of `(Ideal' A K L B)` over `K` --- to be the stabilizer of the MulAction `gal_action_Ideal'`. - -variable {A K L B} in -/-- The decomposition group of `Q : Ideal' A K L B` over `K`. -This is a subgroup of `L ≃ₐ[K] L`. -/ -def decomposition_subgroup_Ideal' (Q : Ideal' A K L B) : - Subgroup (L ≃ₐ[K] L) := MulAction.stabilizer (L ≃ₐ[K] L) Q - --- The following variables introduce instances of the residue fields `(A ⧸ P)` and --- `(B ⧸ Q)` as finite fields. -variable (P : Ideal A) [Ideal.IsMaximal P] [Fintype (A ⧸ P)] (P_ne_bot : P ≠ ⊥) - (Q : Ideal' A K L B) [Ideal.IsMaximal Q] [Fintype (B ⧸ Q)] (Q_ne_bot : Q ≠ (⊥ : Ideal B)) - -- This next line was suggested by Amelia Livingston; mathematically it is - -- equivalent to `P ⊆ A ∩ Q` but it's written purely within the typeclass system. - [Algebra (A ⧸ P) (B ⧸ Q)] [IsScalarTower A (A ⧸ P) (B ⧸ Q)] - -/-- `Fintype.card (A ⧸ P)` -/ -local notation "q" => Fintype.card (A ⧸ P) --- The main existence proof for the Frobenius element will show that mod `Q` it acts as `x ↦ x^q`. - -namespace CRTRepresentative.auxiliary - -variable {A K L B} in -/-- Given an ideal `Q`, we have a map `g ↦ g • Q` from `Gal(L/K)` to `Ideal' B`, -which is constant on right cosets of the decomposition group of `Q` over `K`. -Hence it descends to a map from the space space of cosets to `Ideal' B`; -this descent will be injective and will have image the orbit of `Q`. -/ -noncomputable def f : - ((L ≃ₐ[K] L) ⧸ ( decomposition_subgroup_Ideal' Q)) → - (Ideal' A K L B) := - fun x => Quotient.liftOn' x (fun g => g • Q) <| by - intros σ τ h - rw [QuotientGroup.leftRel_apply] at h - -- h : σ⁻¹ * τ ∈ decomposition_subgroup_Ideal' Q - apply MulAction.mem_stabilizer_iff.1 at h - -- h : (σ⁻¹ * τ) • Q = Q - dsimp only - -- ⊢ σ • Q = τ • Q - rwa [← eq_inv_smul_iff, eq_comm, smul_smul] -- manipulate - -- the goal until it becomes `h`, then `rwa` finishes it. - --- The following instance supplies one hypothesis of the CRT. -instance MapPrimestoPrimes (σ : L ≃ₐ[K] L) (Q : Ideal' A K L B) [Ideal.IsPrime Q] : - Ideal.IsPrime (σ • Q) := Ideal.comap_isPrime (AlgEquiv.symm (galRestrict A K L B σ)) (Q) - -end CRTRepresentative.auxiliary - --- The following lemma supplies another hypothesis of the CRT. -lemma coprime_ideals_non_equal_prime (I J : Ideal' A K L B) [Imax : Ideal.IsMaximal I] - [Jmax : Ideal.IsMaximal J] (h : I ≠ J) : IsCoprime I J := by - rwa [Ideal.isCoprime_iff_sup_eq, Ideal.IsMaximal.coprime_of_ne Imax Jmax] - -section CRTRepresentative --- We `open Classical`, in order to allow us to use the tactic `if then else` -open CRTRepresentative.auxiliary - --- Jujian helped me to write the following lemma and theorem. -/-- There exists an element of `B` which is equal to the generator `g` of `(B ⧸ Q)ˣ` mod -the coset of `Q` in the orbit of `Q` under `(L ≃ₐ[K] L)`, and -equal to `0` mod any other coset. -/ -lemma crt_representative (b : B) (Q_ne_bot : Q ≠ (⊥ : Ideal B)) : ∃ (y : B), - ∀ (i : (L ≃ₐ[K] L) ⧸ decomposition_subgroup_Ideal' Q), - if i = Quotient.mk'' 1 then y - b ∈ f Q i else y ∈ f Q i := by - -- We know that we want `IsDedekindDomain.exists_forall_sub_mem_ideal` to - -- give us the components of the goal, - -- so we assume `IsDedekindDomain.exists_forall_sub_mem_ideal`, - -- and dissect it. - have := IsDedekindDomain.exists_forall_sub_mem_ideal (s := Finset.univ) (f Q) (fun _ ↦ 1) - (fun i _ ↦ by - induction' i using Quotient.inductionOn' with i - -- ⊢ Prime (f Q (Quotient.mk'' i)) - change Prime (i • Q) - apply Ideal.prime_of_isPrime (h := MapPrimestoPrimes A K L B i Q) - contrapose! Q_ne_bot - -- goal: (Q_ne_bot : i • Q = ⊥) → Q = ⊥ - apply_fun (i⁻¹ • ·) at Q_ne_bot -- that's the hint it needs - simpa using Q_ne_bot - ) - (fun i _ j _ hij ↦ by - induction' i using Quotient.inductionOn' with i - induction' j using Quotient.inductionOn' with j - change i • Q ≠ j • Q -- goal is this *by definition* - contrapose! hij - simp only [Quotient.eq''] - rw [QuotientGroup.leftRel_eq] - simp only - symm at hij - rw [←inv_smul_eq_iff, smul_smul] at hij - exact hij - ) - (fun i ↦ if i = ⟨Quotient.mk'' 1, Finset.mem_univ _⟩ then b else 0) - choose y hy using this - use y - peel hy with hy - split_ifs <;> simp_all - -variable {A K L B Q} in -/--"By the Chinese remainder theorem, there exists an element `ρ` of `B` such that -`ρ` generates the group `(B ⧸ Q)ˣ` and lies in `τ • Q` for all `τ` not in the -decomposition subgroup of `Q` over `K`". -/ -theorem exists_generator (Q_ne_bot : Q ≠ (⊥ : Ideal B)) : ∃ (ρ : B) (h : IsUnit (Ideal.Quotient.mk Q ρ)) , - (∀ (x : (B ⧸ Q)ˣ), x ∈ Subgroup.zpowers h.unit) ∧ - (∀ τ : L ≃ₐ[K] L, (τ ∉ decomposition_subgroup_Ideal' Q) → - ρ ∈ (τ • Q)) := by - have i : IsCyclic (B ⧸ Q)ˣ := inferInstance - apply IsCyclic.exists_monoid_generator at i - rcases i with ⟨⟨g, g', hgg', hg'g⟩, hg⟩ - induction' g using Quotient.inductionOn' with g - obtain ⟨ρ , hρ⟩ := crt_representative A K L B Q g Q_ne_bot - use ρ - have eq1 : (Quotient.mk'' ρ : B ⧸ Q) = Quotient.mk'' g := by - specialize hρ (Quotient.mk'' 1) - rw [if_pos rfl] at hρ - delta f at hρ - rw [Quotient.liftOn'_mk'', one_smul] at hρ - simp only [Submodule.Quotient.mk''_eq_mk, Ideal.Quotient.mk_eq_mk] - rwa [Ideal.Quotient.eq] - refine ⟨⟨⟨Quotient.mk'' g, g', hgg', hg'g⟩, eq1.symm⟩, ?_, ?_⟩ - · intro x - specialize hg x - set u := _; change x ∈ Subgroup.zpowers u - suffices equ : u = ⟨Quotient.mk'' g, g', hgg', hg'g⟩ by - rwa [equ, ← mem_powers_iff_mem_zpowers]; - ext - simpa only [IsUnit.unit_spec, Submodule.Quotient.mk''_eq_mk, Ideal.Quotient.mk_eq_mk] - · intro τ hτ - specialize hρ (Quotient.mk'' τ) - have neq1 : - (Quotient.mk'' τ : (L ≃ₐ[K] L) ⧸ decomposition_subgroup_Ideal' Q) ≠ - Quotient.mk'' 1 := by - contrapose! hτ - simpa only [Quotient.eq'', QuotientGroup.leftRel_apply, mul_one, inv_mem_iff] using hτ - rw [if_neg neq1] at hρ - delta f at hρ - rwa [Quotient.liftOn'_mk''] at hρ - -end CRTRepresentative - -section GalActionIdeal'Supplementary - -variable {A K L B Q} - --- this lemma written by Amelia -lemma smul_ideal_eq_map (g : L ≃ₐ[K] L) (I : Ideal' A K L B) : - g • I = Ideal.map (galRestrict A K L B g) I := - Ideal.comap_symm (galRestrict A K L B g).toRingEquiv - -lemma mem_smul_ideal_iff (g : L ≃ₐ[K] L) (I : Ideal' A K L B) (x : B) : - x ∈ g • I ↔ (galRestrict A K L B g).symm x ∈ I := Iff.rfl - -lemma mem_decomposition_iff (g : L ≃ₐ[K] L) : - g ∈ decomposition_subgroup_Ideal' Q ↔ ∀ x, x ∈ Q ↔ - (galRestrict A K L B g) x ∈ Q := by - change g • Q = Q ↔ _ - rw [SetLike.ext_iff] - simp only [mem_smul_ideal_iff] - constructor - · intros h x - constructor - · intro h1 - specialize h ((galRestrict A K L B) g x) - simp only [AlgEquiv.symm_apply_apply] at h - apply h.1 at h1 - exact h1 - · intro h2 - specialize h ((galRestrict A K L B) g x) - simp only [AlgEquiv.symm_apply_apply] at h - apply h.2 at h2 - exact h2 - · intros h x - constructor - · intro h1 - specialize h (((galRestrict A K L B) g).symm x) - simp only [AlgEquiv.apply_symm_apply] at h - apply h.1 at h1 - exact h1 - · intro h2 - specialize h (((galRestrict A K L B) g).symm x) - simp only [AlgEquiv.apply_symm_apply] at h - apply h.2 at h2 - exact h2 - -end GalActionIdeal'Supplementary - -open Polynomial BigOperators - -/-! ## Freshman's Dream -We show `"q" => Fintype.card (A ⧸ P)` is `p ^ n` for some `(n : ℕ)`, where -`p := Char P (A ⧸ P)`. -Thence, by the ``Freshman's Dream``, for `a : A[X]`, -we have `a(X ^ q) ≡ a(X) ^ q mod P`. -/ -section FreshmansDream - -variable {A K L B Q} - --- local notation "q" => Fintype.card (A ⧸ P) -- show this is a power of a prime -noncomputable instance : Field (A ⧸ P) := Ideal.Quotient.field P - -lemma is_primepow_char_A_quot_P : IsPrimePow q := Fintype.isPrimePow_card_of_field - -lemma ex_primepow_char_A_quot_P : ∃ p n : ℕ , Prime p ∧ 0 < n ∧ p ^ n = q := by - exact is_primepow_char_A_quot_P _ - -local notation "p" => Classical.choose (CharP.exists (A ⧸ P)) -local notation "p'" => Classical.choose (ex_primepow_char_A_quot_P P) -local notation "n" => Classical.choose (Classical.choose_spec (ex_primepow_char_A_quot_P P)) - -instance p_is_char : CharP (A ⧸ P) p := Classical.choose_spec (CharP.exists (A ⧸ P)) - -lemma p_is_prime : (Nat.Prime p) := CharP.char_prime_of_ne_zero (A ⧸ P) <| - CharP.char_ne_zero_of_finite (A ⧸ P) _ - -lemma p'_is_prime : Nat.Prime p' := - Nat.prime_iff.mpr <| (ex_primepow_char_A_quot_P P).choose_spec.choose_spec.1 - -lemma q_is_p'_pow_n : p' ^ n = q := - Classical.choose_spec (Classical.choose_spec (ex_primepow_char_A_quot_P P)) |>.2.2 - -lemma p_is_p' : p = p' := by - -- `q = 0` in `A⧸ P` and `p | q` since `CharP p` then since `q = p' ^ n` then `p' = p` - have eq0 : (q : A⧸ P) = 0 := Nat.cast_card_eq_zero (A ⧸ P) - have h1 : p ∣ q := charP_iff (A ⧸ P) p |>.1 (p_is_char P) q |>.1 eq0 - have eq1 : p' ^ n = q := q_is_p'_pow_n P - rw [← eq1] at h1 - exact Nat.dvd_prime (p'_is_prime P) |>.1 - (Nat.Prime.dvd_of_dvd_pow (p_is_prime P) h1) |>.resolve_left <| Nat.Prime.ne_one <| p_is_prime P - -lemma q_is_p_pow_n : p ^ n = q := by - rw [p_is_p', q_is_p'_pow_n] - -/-- By the ``Freshman's Dream``, for `a : A[X]`, -we have `a(X ^ q) ≡ a(X) ^ q mod P,` where -`q` is the cardinality of the residue field `(A ⧸ P)`. -/ -theorem pow_eq_expand (a : (A ⧸ P)[X]) : - (a ^ q) = (expand _ q a) := by - have pprime : Nat.Prime p := p_is_prime P - have factprime : Fact (Nat.Prime p) := { out := pprime } - rw [← q_is_p_pow_n, ← map_expand_pow_char, map_expand, FiniteField.frobenius_pow] - · simp [exists_and_left, RingHom.one_def, map_id] - · exact (q_is_p_pow_n P).symm - -end FreshmansDream - -section generator - -variable {A K L B Q} - -/-- `α` is an element of `B` such that `IsUnit (Ideal.Quotient.mk Q α))`, -`α` generates the group `(B ⧸ Q)ˣ)`; and -`∀ τ : L ≃ₐ[K] L, (τ ∉ decomposition_subgroup_Ideal' A K L B Q), -α ∈ (τ • Q)))`. -/ -noncomputable def generator : B := - Classical.choose (exists_generator Q_ne_bot) - --- Jujian suggested and helped with the following lemmas: -lemma generator_isUnit : IsUnit (Ideal.Quotient.mk Q (generator Q_ne_bot)) := - (Classical.choose_spec (exists_generator Q_ne_bot)).choose - -lemma generator_mem_zpowers : - ∀ (x : (B ⧸ Q)ˣ), x ∈ Subgroup.zpowers (generator_isUnit Q_ne_bot).unit := - (Classical.choose_spec (exists_generator Q_ne_bot)).choose_spec.1 - -lemma generator_mem_submonoid_powers (x : (B ⧸ Q)ˣ) : - x ∈ Submonoid.powers (generator_isUnit Q_ne_bot).unit := by - classical - have h := IsCyclic.image_range_orderOf (generator_mem_zpowers Q_ne_bot) - have hx : x ∈ Finset.univ := by simp only [Finset.mem_univ] - rw [← h] at hx - simp only [Finset.mem_image, Finset.mem_range] at hx - rcases hx with ⟨n, _, hn2⟩ - use n - -lemma generator_well_defined : (∀ τ : L ≃ₐ[K] L, (τ ∉ decomposition_subgroup_Ideal' Q) → - (generator Q_ne_bot) ∈ (τ • Q)) := - (Classical.choose_spec (exists_generator Q_ne_bot)).choose_spec.2 - -end generator - -/-- `generator A K L B Q Q_ne_bot` -/ -local notation "α" => generator Q_ne_bot - -open BigOperators - --- Jujian helped with the following def: -/-- `F : B[X]` defined to be a product of linear factors `(X - τ • α)`; where -`τ` runs over `L ≃ₐ[K] L`, and `α : B` is an element which generates `(B ⧸ Q)ˣ` -and lies in `τ • Q` for all `τ ∉ (decomposition_subgroup_Ideal' A K L B Q)`.-/ -noncomputable def F' : B[X] := ∏ τ : L ≃ₐ[K] L, - (X - C (galRestrict A K L B τ α)) - -/-- `F' A K L B Q Q_ne_bot` -/ -local notation "F" => F' A K L B Q Q_ne_bot - -variable [IsGalois K L] [IsIntegralClosure A A K] - -namespace coeff_lives_in_A.auxiliary -/-- The action of automorphisms `σ : L ≃ₐ[K] L` on linear factors of `F` acts as -scalar multiplication on the constants `C (galRestrict A K L B τ (α))`. -/ -theorem gal_smul_F_eq (σ : L ≃ₐ[K] L) : - galRestrict A K L B σ • - (∏ τ : L ≃ₐ[K] L, - (X - C (galRestrict A K L B τ α))) = - ∏ τ : L ≃ₐ[K] L, - (X - C (galRestrict A K L B σ - (galRestrict A K L B τ α))):= by - simp [Finset.smul_prod', smul_sub, smul_X, smul_C, AlgEquiv.smul_def] - -/-- use `Finset.prod_bij` to show -`(galRestrict A K L B σ • (∏ τ : L ≃ₐ[K] L, (X - C (galRestrict A K L B τ α))) = -(∏ τ : L ≃ₐ[K] L, (X - C (galRestrict A K L B τ α)))` -/ -lemma F_invariant_under_finite_aut (σ : L ≃ₐ[K] L) : - ∏ τ : L ≃ₐ[K] L, (X - C (galRestrict A K L B σ - (galRestrict A K L B τ α))) = F := by - set i : (τ : L ≃ₐ[K] L) → τ ∈ Finset.univ → L ≃ₐ[K] L := fun τ _ => σ * τ - -- needed to use `set i` instead of `have i`, in order to be able to use `i` later on, in proof - have hi : ∀ (τ : L ≃ₐ[K] L) (hτ : τ ∈ Finset.univ), i τ hτ ∈ Finset.univ := by - simp only [Finset.mem_univ, forall_true_left, forall_const] - have i_inj : ∀ (τ₁ : L ≃ₐ[K] L) (hτ₁ : τ₁ ∈ Finset.univ) (τ₂ : L ≃ₐ[K] L) - (hτ₂ : τ₂ ∈ Finset.univ), i τ₁ hτ₁ = i τ₂ hτ₂ → τ₁ = τ₂ := by - intros τ₁ _ τ₂ _ h - simpa [i, mul_right_inj] using h - have i_surj : ∀ σ ∈ Finset.univ, ∃ (τ : L ≃ₐ[K] L) (hτ : τ ∈ Finset.univ), i τ hτ = σ := by - intro τ' - simp only [Finset.mem_univ, exists_true_left, forall_true_left, i] - use (σ⁻¹ * τ') - group - have h : ∀ (τ : L ≃ₐ[K] L) (hτ : τ ∈ Finset.univ), - (X - C (galRestrict A K L B σ (galRestrict A K L B τ α))) = - (X - C (galRestrict A K L B (i τ hτ) α)) := by - intros τ hτ - simp only [i, map_mul, sub_right_inj, C_inj] - rw [AlgEquiv.aut_mul] - rfl - exact Finset.prod_bij i hi i_inj i_surj h - -/-- ` L ≃ₐ[K] L` fixes `F`. -/ -theorem gal_smul_F_eq_self (σ : L ≃ₐ[K] L) : - galRestrict A K L B σ • (∏ τ : L ≃ₐ[K] L, - (X - C (galRestrict A K L B τ α))) = - (∏ τ : L ≃ₐ[K] L, (X - C (galRestrict A K L B τ α))) := by - rw [gal_smul_F_eq, F_invariant_under_finite_aut] - rfl - -theorem gal_smul_coeff_eq (n : ℕ) (h : ∀ σ : L ≃ₐ[K] L, galRestrict A K L B σ • F = F) - (σ : L ≃ₐ[K] L) : galRestrict A K L B σ • (coeff F n) = coeff F n := by - nth_rewrite 2 [← h σ] - simp [coeff_smul, AlgEquiv.smul_def] - -variable {A K L B Q} - -theorem coeff_lives_in_fixed_field (n : ℕ) : - (algebraMap B L (coeff F n : B) : L) ∈ - IntermediateField.fixedField (⊤ : Subgroup (L ≃ₐ[K] L)) := by - change ∀ _, _ - rintro ⟨σ, -⟩ - change σ _ = _ - rw [← algebraMap_galRestrict_apply A] - have h := gal_smul_F_eq_self A K L B Q Q_ne_bot σ - apply_fun (coeff · n) at h - rw [coeff_smul] at h - change (galRestrict A K L B) σ (coeff F n) = coeff F n at h - congr 1 - -lemma coeff_lives_in_K (n : ℕ) : ∃ k : K, algebraMap B L (coeff F n) = (algebraMap K L k) := by - have eq0 := ((@IsGalois.tfae K _ L _ _ _).out 0 1).mp (by infer_instance) - have h := coeff_lives_in_fixed_field Q_ne_bot n - rw [eq0] at h - change _ ∈ (⊥ : Subalgebra _ _) at h - rw [Algebra.mem_bot] at h - obtain ⟨k, hk⟩ := h - exact ⟨_, hk.symm⟩ - -end coeff_lives_in_A.auxiliary - -variable {A K L B Q} - -open coeff_lives_in_A.auxiliary in -theorem coeff_lives_in_A (n : ℕ) : ∃ a : A, algebraMap B L (coeff F n) = (algebraMap A L a) := by - obtain ⟨k, hk⟩ := coeff_lives_in_K Q_ne_bot n - have h1 := IsIntegralClosure.isIntegral_iff (A := A) (R := A) (B := K) (x := k) - obtain ⟨p, p_monic, hp⟩ := IsIntegralClosure.isIntegral_iff - (A := B) (R := A) (B := L) (x := (algebraMap B L) (coeff F n)) |>.mpr ⟨coeff F n, rfl⟩ - have eq0 : algebraMap A L = (algebraMap K L).comp (algebraMap A K) := by - ext - exact (IsScalarTower.algebraMap_apply A K L _) - have h2 : IsIntegral A k := by - refine ⟨p, p_monic, ?_⟩ - rw [hk, eq0, ← Polynomial.hom_eval₂] at hp - apply (map_eq_zero_iff _ _).1 hp - exact NoZeroSMulDivisors.algebraMap_injective K L - cases' h1.1 h2 with a' ha' - use a' - simpa [eq0, RingHom.coe_comp, Function.comp_apply, ha'] - -/-- `α` is a root of `F`. -/ -lemma isRoot_α : eval α F = 0 := by - have evalid : eval α (X - C ((α))) = 0 := by - simp only [eval_sub, eval_X, eval_C, sub_self] - have eqF : (eval α (∏ τ : L ≃ₐ[K] L, - (X - C (galRestrict A K L B τ α)))) = eval α F := rfl - have eq0 : (eval α (X - C ((α))) = 0) → (eval α (∏ τ : L ≃ₐ[K] L, - (X - C (galRestrict A K L B τ α))) = 0) := by - intro _ - rw [Polynomial.eval_prod] - simp only [eval_sub, eval_X, eval_C] - apply Finset.prod_eq_zero_iff.2 - use 1 - constructor - · simp only [Finset.mem_univ] - · simp only [map_one] - change α - α = 0 - rw [sub_self] - apply eq0 at evalid - rwa [← eqF] - -lemma quotient_isRoot_α : (eval α F) ∈ Q := (isRoot_α Q_ne_bot) ▸ Ideal.zero_mem _ - -lemma conjugate_isRoot_α (σ : L ≃ₐ[K] L) : (eval (galRestrict A K L B σ α) F) = 0 := by - have evalσ : eval (galRestrict A K L B σ α) - (X - C (galRestrict A K L B σ α)) = 0 := by - simp [eval_sub, eval_X, eval_C, sub_self] - have eqF : (eval (galRestrict A K L B σ α) (∏ τ : L ≃ₐ[K] L, - (X - C (galRestrict A K L B τ α)))) = - eval (galRestrict A K L B σ α) F := rfl - have eq0 : (eval (galRestrict A K L B σ α) - (X - C (galRestrict A K L B σ α)) = 0) → - ((eval (galRestrict A K L B σ α) (∏ τ : L ≃ₐ[K] L, - (X - C (galRestrict A K L B τ α)))) = 0) := by - intro _ - rw [Polynomial.eval_prod] - simp only [eval_sub, eval_X, eval_C] - apply Finset.prod_eq_zero_iff.2 - use σ - constructor - · simp only [Finset.mem_univ] - · simp only [sub_self] - apply eq0 at evalσ - rw [← eqF, evalσ] - -lemma conjugate_quotient_isRoot_α (σ : L ≃ₐ[K] L) : - (eval (galRestrict A K L B σ α) F) ∈ Q := (conjugate_isRoot_α Q_ne_bot) _ ▸ Ideal.zero_mem _ - -lemma F_is_root_iff_is_conjugate {x : B} : - IsRoot F x ↔ (∃ σ : L ≃ₐ[K] L, x = (galRestrict A K L B σ α)) := by - constructor - · intro h - rw [Polynomial.IsRoot.def] at h - have eqF : eval x (∏ τ : L ≃ₐ[K] L, - (X - C ((galRestrict A K L B τ) α))) = - eval x F := rfl - rw [← eqF, Polynomial.eval_prod] at h - suffices _ : ∃ σ : L ≃ₐ[K] L, eval x (X - C ((((galRestrict A K L B) σ)) α)) = 0 by - rw [Finset.prod_eq_zero_iff] at h - rcases h with ⟨a, _, ha2⟩ - rw [← Polynomial.IsRoot.def] at ha2 - apply Polynomial.root_X_sub_C.1 at ha2 - use a - exact ha2.symm - rw [Finset.prod_eq_zero_iff] at h - rcases h with ⟨a', _, haa2⟩ - use a' - · intros h - rcases h with ⟨σ, hσ⟩ - rw [Polynomial.IsRoot.def, hσ] - exact conjugate_isRoot_α Q_ne_bot _ - -lemma F_eval_zero_is_conjugate {x : B} (h : eval x F = 0) : ∃ σ : L ≃ₐ[K] L, - x = ((galRestrict A K L B σ) α) := by - rwa [← Polynomial.IsRoot.def, F_is_root_iff_is_conjugate] at h - --- make a polynomial with coefficients in `A` -lemma ex_poly_in_A : ∃ m : A[X], Polynomial.map (algebraMap A B) m = F := by - have h (n : ℕ) : ∃ a : A, algebraMap B L (coeff F n) = (algebraMap A L a) := - coeff_lives_in_A Q_ne_bot n - let m : A[X] := { - toFinsupp := { - support := Polynomial.support F - toFun := fun n => Classical.choose (h n) - mem_support_toFun := by - intro n - simp only [mem_support_iff, ne_eq] - have := Classical.choose_spec (h n) - set s := Classical.choose (h n) - apply Iff.not - rw [← _root_.map_eq_zero_iff (algebraMap B L), this, map_eq_zero_iff] - have I : NoZeroSMulDivisors A L := NoZeroSMulDivisors.trans A K L - · exact NoZeroSMulDivisors.algebraMap_injective _ _ - · exact NoZeroSMulDivisors.algebraMap_injective _ _ - }} - use m - ext n - simp only [coeff_map, coeff_ofFinsupp, Finsupp.coe_mk] - set s := Classical.choose (h n) - apply NoZeroSMulDivisors.algebraMap_injective B L - exact (Classical.choose_spec (h n)) ▸ (IsScalarTower.algebraMap_apply A B L _).symm - -/--`m' : A[X]` such that `Polynomial.map (algebraMap A B) m = F`. -/ -noncomputable def m' : A[X] := Classical.choose (ex_poly_in_A Q_ne_bot) - -local notation "m" => m' Q_ne_bot - -lemma m_mapsto_F : Polynomial.map (algebraMap A B) m = F := - Classical.choose_spec (ex_poly_in_A Q_ne_bot) - -lemma m_eq_F_in_B_quot_Q : - Polynomial.map (algebraMap B (B ⧸ Q)) (Polynomial.map (algebraMap A B) m) = - Polynomial.map (algebraMap B (B ⧸ Q)) F := by - suffices h : Polynomial.map (algebraMap A B) m = F by - exact congrArg (map (algebraMap B (B ⧸ Q))) h - exact m_mapsto_F _ - -lemma m_expand_char_q : (Polynomial.map (algebraMap A (A ⧸ P)) m) ^ q = - (expand _ q (Polynomial.map (algebraMap A (A ⧸ P)) m)) := by - exact pow_eq_expand _ _ - -lemma B_m_expand_char_q : (Polynomial.map (algebraMap A (B ⧸ Q)) m) ^ q = - (expand _ q (Polynomial.map (algebraMap A (B ⧸ Q)) m)) := by - have st : (algebraMap A (B ⧸ Q)) = - RingHom.comp (algebraMap (A ⧸ P) (B ⧸ Q)) (algebraMap A (A ⧸ P)) := - IsScalarTower.algebraMap_eq A (A ⧸ P) (B ⧸ Q) - rw [st, ← Polynomial.map_map, ← Polynomial.map_pow, m_expand_char_q, map_expand] - -lemma A_B_scalar_tower_m : Polynomial.map (algebraMap A (B ⧸ Q)) m = - Polynomial.map (RingHom.comp (algebraMap B (B ⧸ Q)) (algebraMap A B)) m := by - have st : (algebraMap A (B ⧸ Q)) = - RingHom.comp (algebraMap B (B ⧸ Q)) (algebraMap A B) := - IsScalarTower.algebraMap_eq A B (B ⧸ Q) - rw [st] - -lemma pow_expand_A_B_scalar_tower_m : - (( Polynomial.map ( RingHom.comp (algebraMap B (B ⧸ Q)) (algebraMap A B))) m) ^ q = - (expand _ q ( Polynomial.map ( RingHom.comp (algebraMap B (B ⧸ Q)) (algebraMap A B) ) m)) := by - have h : (Polynomial.map (algebraMap A (B ⧸ Q)) m) ^ q = - (expand _ q (Polynomial.map (algebraMap A (B ⧸ Q)) m)) := B_m_expand_char_q P Q_ne_bot - rwa [← A_B_scalar_tower_m] - -lemma pow_expand_A_B_scalar_tower_F : - ( Polynomial.map (algebraMap B (B ⧸ Q)) F) ^ q = - (expand _ q ( Polynomial.map (algebraMap B (B ⧸ Q)) F)) := by - have h : (( Polynomial.map ( RingHom.comp (algebraMap B (B ⧸ Q)) (algebraMap A B))) m) ^ q = - (expand _ q ( Polynomial.map ( RingHom.comp (algebraMap B (B ⧸ Q)) (algebraMap A B) ) m)) := - pow_expand_A_B_scalar_tower_m P Q_ne_bot - rwa [← m_mapsto_F, Polynomial.map_map] - -lemma F_expand_eval_eq_eval_pow : - (eval₂ (Ideal.Quotient.mk Q) (Ideal.Quotient.mk Q α) F) ^ q = - (eval₂ (Ideal.Quotient.mk Q) (Ideal.Quotient.mk Q (α ^ q)) F) := by - simp_rw [← Polynomial.eval_map, ← Ideal.Quotient.algebraMap_eq, ← Polynomial.coe_evalRingHom, - ← map_pow, pow_expand_A_B_scalar_tower_F, Ideal.Quotient.algebraMap_eq, coe_evalRingHom, - expand_eval, map_pow] - -lemma quotient_F_is_product_of_quot : - (Polynomial.map (Ideal.Quotient.mk Q) F) = - ∏ τ : L ≃ₐ[K] L, (X - C ((Ideal.Quotient.mk Q) ((galRestrict A K L B τ) α))) := by - rw [← Polynomial.coe_mapRingHom] - erw [map_prod] - simp [map_sub, coe_mapRingHom, map_X, map_C] - -lemma quotient_F_is_root_iff_is_conjugate (x : (B ⧸ Q)) : - IsRoot (Polynomial.map (Ideal.Quotient.mk Q) F) x ↔ - (∃ σ : L ≃ₐ[K] L, x = ((Ideal.Quotient.mk Q) ((galRestrict A K L B σ) α))) := by - rw [quotient_F_is_product_of_quot, Polynomial.isRoot_prod] - simp only [Finset.mem_univ, eval_sub, eval_X, eval_C, true_and, Polynomial.root_X_sub_C] - simp [eq_comm] - -lemma pow_eval_root_in_Q : ((eval α F) ^ q) ∈ Q := by - have h : (eval α F) ∈ Q := quotient_isRoot_α Q_ne_bot - apply Ideal.pow_mem_of_mem - · exact h - · exact Fintype.card_pos - -lemma expand_eval_root_eq_zero : - (eval₂ (Ideal.Quotient.mk Q) (Ideal.Quotient.mk Q (α ^ q)) F) = 0 := by - simp only [← F_expand_eval_eq_eval_pow P Q_ne_bot, eval₂_at_apply, ne_eq, Fintype.card_ne_zero, - not_false_eq_true, pow_eq_zero_iff] - have h : eval α F ∈ Q := quotient_isRoot_α Q_ne_bot - rwa [← Ideal.Quotient.eq_zero_iff_mem] at h - --- now, want `∃ σ, α ^ q ≡ σ α mod Q` -lemma pow_q_is_conjugate : ∃ σ : L ≃ₐ[K] L, (Ideal.Quotient.mk Q (α ^ q)) = - (Ideal.Quotient.mk Q ((((galRestrict A K L B) σ)) α)) := by - rw [← quotient_F_is_root_iff_is_conjugate, map_pow, IsRoot.def, Polynomial.eval_map] - exact expand_eval_root_eq_zero P Q_ne_bot - --- following lemma suggested by Amelia -lemma pow_quotient_IsRoot_α : (eval (α ^ q) F) ∈ Q := by - rw [← Ideal.Quotient.eq_zero_iff_mem] - have h2 : (eval₂ (Ideal.Quotient.mk Q) (Ideal.Quotient.mk Q (α ^ q)) F) = 0 := - expand_eval_root_eq_zero P Q_ne_bot - convert h2 - rw [eval₂_at_apply] - -/--`α ^ q ≡ σ • α mod Q` for some `σ : L ≃ₐ[K] L` -/ -lemma pow_q_conjugate : - ∃ σ : L ≃ₐ[K] L, (α ^ q - (galRestrict A K L B σ) α) ∈ Q := by - convert pow_q_is_conjugate P Q_ne_bot - rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem] - -/--`Frob' : L ≃ₐ[K] L` such that ` (α ^ q - (galRestrict A K L B σ) α) ∈ Q`. -/ -noncomputable def Frob' : L ≃ₐ[K] L := Classical.choose (pow_q_conjugate P Q_ne_bot) - -local notation "Frob" => Frob' P Q_ne_bot - -/-- if `Frob ∉ decomposition_subgroup_Ideal' A K L B Q`, then `Frob⁻¹ • Q ≠ Q` -/ -lemma inv_aut_not_mem_decomp (h : Frob ∉ decomposition_subgroup_Ideal' Q) : (Frob⁻¹ • Q) ≠ Q := by - by_contra con - apply inv_smul_eq_iff.1 at con - exact h (id con.symm) - -/-- `α ∈ Frob⁻¹ • Q`. -/ -lemma gen_zero_mod_inv_aut (h1 : Frob ∉ decomposition_subgroup_Ideal' Q) : - α ∈ (Frob⁻¹ • Q) := by - have inv : Frob⁻¹ ∉ decomposition_subgroup_Ideal' Q := by - simpa [inv_mem_iff] - exact generator_well_defined _ _ inv - -lemma prop_Frob : (α ^ q - (galRestrict A K L B Frob) α) ∈ Q := - Classical.choose_spec (pow_q_conjugate P Q_ne_bot) - --- proof of this lemma written by Amelia: -lemma inv_Frob (h : α ∈ (Frob⁻¹ • Q)) : ((galRestrict A K L B Frob) α) ∈ Q := by - change (galRestrict A K L B Frob⁻¹).symm α ∈ Q at h - simp_all only [ne_eq, map_inv] - convert h - -/-- If `α ∈ Frob⁻¹ • Q`, then `α ^ q ≡ Frob • α ≡ 0 mod Q.` -/ -lemma is_zero_pow_gen_mod_Q (h : α ∈ (Frob⁻¹ • Q)) : - (α ^ q) ∈ Q := by - have h1 : (galRestrict A K L B Frob) α ∈ Q := inv_Frob P Q_ne_bot h - have h2 : (α ^ q - (galRestrict A K L B Frob) α) ∈ Q := - Classical.choose_spec (pow_q_conjugate P Q_ne_bot) - rw [← Ideal.neg_mem_iff] at h1 - have h3 : ((α ^ q - (galRestrict A K L B Frob) α) - - (-(galRestrict A K L B Frob) α)) ∈ Q := by - exact Ideal.sub_mem Q h2 h1 - convert h3 - simp [sub_neg_eq_add, sub_add_cancel] - -/-- `Frob ∈ decomposition_subgroup_Ideal' A K L B Q`. -/ -theorem Frob_is_in_decompositionSubgroup : - Frob ∈ decomposition_subgroup_Ideal' Q := by - by_contra con - apply IsUnit.ne_zero <| generator_isUnit Q_ne_bot - exact Ideal.Quotient.eq_zero_iff_mem.2 <| - Ideal.IsPrime.mem_of_pow_mem (hI := inferInstance) - (H := is_zero_pow_gen_mod_Q (h := gen_zero_mod_inv_aut (h1 := con))) - -/- ## Now, for `γ : B` we have two cases: `γ ∉ Q` and `γ ∈ Q`. -/ - -/-- Every element `γ : B`, `γ ∉ Q`, can be written `γ = α ^ i + β`, with `β ∈ Q` -/ -lemma γ_not_in_Q_is_pow_gen {γ : B} (h : γ ∉ Q) : ∃ (i : ℕ), γ - (α ^ i) ∈ Q := by - let g := Units.mk0 (((Ideal.Quotient.mk Q γ))) <| by - intro h1 - rw [Ideal.Quotient.eq_zero_iff_mem] at h1 - exact h h1 - rcases generator_mem_submonoid_powers Q_ne_bot g with ⟨i, hi⟩ - use i - rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem] - simp [g, Units.ext_iff, Units.val_pow_eq_pow_val, IsUnit.unit_spec, Units.val_mk0] at hi - simp [g, map_pow, hi] - -/--`i' : ℕ` such that, for `(γ : B) (h : γ ∉ Q)`, `γ - (α ^ i) ∈ Q`. -/ -noncomputable def i' {γ : B} (h : γ ∉ Q) : ℕ := - (Classical.choose (γ_not_in_Q_is_pow_gen Q_ne_bot h)) - -local notation "i" => i' Q_ne_bot - -lemma prop_γ_not_in_Q_is_pow_gen {γ : B} (h : γ ∉ Q) : γ - (α ^ (i h)) ∈ Q := - (γ_not_in_Q_is_pow_gen Q_ne_bot h).choose_spec - -/-- `Frob • γ ≡ Frob • (α ^ i) mod Q` -/ -lemma eq_pow_gen_apply {γ : B} (h: γ ∉ Q) : (galRestrict A K L B Frob) γ - - galRestrict A K L B Frob (α ^ (i h)) ∈ Q := by - rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem] - have h1 : γ - (α ^ (i h)) ∈ Q := prop_γ_not_in_Q_is_pow_gen Q_ne_bot h - rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.Quotient.eq] at h1 - rw [Ideal.Quotient.eq, ← map_sub] - have := Frob_is_in_decompositionSubgroup P Q_ne_bot - rw [mem_decomposition_iff] at this - exact (this _).1 h1 - --- γ ∈ B \ Q is α^i mod Q -/-- `Frob • (α ^ i) ≡ α ^ (i * q) mod Q` -/ -lemma pow_pow_gen_eq_pow_gen_apply {γ : B} {h : γ ∉ Q} : ((α ^ ((i h) * q)) - - galRestrict A K L B Frob (α ^ (i h))) ∈ Q := by - have h1 : α ^ q - (galRestrict A K L B Frob) α ∈ Q := prop_Frob P Q_ne_bot - simp_all only [ne_eq, ← Ideal.Quotient.mk_eq_mk_iff_sub_mem, map_pow] - rw [pow_mul'] - exact congrFun (congrArg HPow.hPow h1) (i h) - -/-- `α ^ (i * q) ≡ γ ^ q mod Q` -/ -lemma pow_pow_gen_eq_pow {γ : B} (h : γ ∉ Q) : ((α ^ ((i h) * q)) - - (γ ^ q)) ∈ Q := by - rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem] - have h1 : γ - (α ^ (i h)) ∈ Q := prop_γ_not_in_Q_is_pow_gen Q_ne_bot h - rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem] at h1 - rw [mul_comm, pow_mul'] - simp only [map_pow] - exact congrFun (congrArg HPow.hPow (id h1.symm)) q - -/-- Case `γ ∉ Q` : then `Frob γ ≡ γ ^ q mod Q`. -/ -theorem Frob_γ_not_in_Q_is_pow {γ : B} (h : γ ∉ Q) : - ((γ ^ q) - (galRestrict A K L B Frob) γ) ∈ Q := by - have h2 : (galRestrict A K L B Frob) γ - - (galRestrict A K L B Frob) (α ^ (i h)) ∈ Q := eq_pow_gen_apply P Q_ne_bot h - have h3 : ((α ^ ((i h) * q)) - - (galRestrict A K L B Frob) (α ^ (i h))) ∈ Q := pow_pow_gen_eq_pow_gen_apply P Q_ne_bot - have h4 : ((α ^ ((i h) * q)) - (γ ^ q)) ∈ Q := pow_pow_gen_eq_pow P Q_ne_bot h - have h5 : (((galRestrict A K L B Frob) γ - - (galRestrict A K L B Frob) (α ^ (i h))) - ( ((α ^ ((i h) * q)) - - (galRestrict A K L B Frob) (α ^ (i h))))) ∈ Q := by - apply Ideal.sub_mem - · exact h2 - · exact h3 - simp only [map_pow, sub_sub_sub_cancel_right] at h5 - have h6 : (( (((galRestrict A K L B) Frob)) γ - α ^ (i h * q)) + - (((α ^ ((i h) * q)) - (γ ^ q)))) ∈ Q := Ideal.add_mem _ h5 h4 - simp only [sub_add_sub_cancel] at h6 - rw [← Ideal.neg_mem_iff] at h6 - simp only [neg_sub] at h6 - exact h6 - -/- ## Now, we consider the case `γ : Q`.-/ - -/-- Case `γ ∈ Q` : then `Frob γ ≡ γ ^ q mod Q`. -/ -theorem Frob_γ_in_Q_is_pow {γ : B} (h : γ ∈ Q) : - ((γ ^ q) - (galRestrict A K L B Frob) γ) ∈ Q := by - apply Ideal.sub_mem - · apply Ideal.pow_mem_of_mem at h - specialize h q - apply h - exact Fintype.card_pos - · exact ((mem_decomposition_iff Frob).1 - (Frob_is_in_decompositionSubgroup P Q_ne_bot) γ).1 h - -lemma for_all_gamma (γ : B) : ((γ ^ q) - (galRestrict A K L B Frob) γ) ∈ Q := by - have h1 : if (γ ∉ Q) then ((γ ^ q) - (galRestrict A K L B Frob) γ) ∈ Q - else ((γ ^ q) - (galRestrict A K L B Frob) γ) ∈ Q := by - split_ifs with H - · apply Frob_γ_in_Q_is_pow P Q_ne_bot at H - simp only at H - convert H - · apply Frob_γ_not_in_Q_is_pow P Q_ne_bot at H - exact H - aesop - -#exit - -/--Let `L / K` be a finite Galois extension of number fields, and let `Q` be a prime ideal -of `B`, the ring of integers of `L`. Then, there exists an element `σ : L ≃ₐ[K] L` -such that `σ` is in the decomposition subgroup of `Q` over `K`; -and `∀ γ : B`, `(γ ^ q) - (galRestrict A K L B σ) γ) ∈ Q`, -i.e., `σγ ≡ γ ^ q mod Q`; -where `q` is the number of elements in the residue field `(A ⧸ P)`, -`P = Q ∩ K`, and `A` is the ring of integers of `K`. -/ -theorem exists_frobenius : - ∃ σ : L ≃ₐ[K] L, - (σ ∈ decomposition_subgroup_Ideal' Q ) ∧ - (∀ γ : B, ((γ ^ q) - (galRestrict A K L B σ) γ) ∈ Q) := - ⟨Frob, Frob_is_in_decompositionSubgroup P Q_ne_bot, fun γ => for_all_gamma P Q_ne_bot γ⟩ - -end FiniteFrobeniusDef diff --git a/FLT/MathlibExperiments/Frobenius2.lean b/FLT/MathlibExperiments/Frobenius2.lean deleted file mode 100644 index a47350f6..00000000 --- a/FLT/MathlibExperiments/Frobenius2.lean +++ /dev/null @@ -1,292 +0,0 @@ -/- -Copyright (c) 2024 Jou Glasheen. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jou Glasheen, Amelia Livingston, Jujian Zhang, Kevin Buzzard --/ -import Mathlib.FieldTheory.Cardinality -import Mathlib.RingTheory.DedekindDomain.Ideal -import Mathlib.RingTheory.Ideal.Pointwise -import Mathlib.RingTheory.IntegralClosure.IntegralRestrict - -/- - - -# DO NOT FIX THIS FILE IF IT BREAKS. - -It is work in progress. If it breaks just move the #exit up to -just before it breaks. Frobenius elements need a complete refactor -so keeping this code up to date is a waste of time. - -# Frobenius elements - -Frobenius elements in Galois groups. - -## Statement of the theorem - -Say `L/K` is a finite Galois extension of number fields, with integer rings `B/A`, -and say `Q` is a maximal ideal of `B` dividing `P` of `A`. This file contains the -construction of an element `Frob Q` in `Gal(L/K)`, and a proof that -modulo `Q` it raises elements to the power `q := |A/P|`. - -More generally, our theory works in the "ABKL" setting, with `B/A` a finite extension of -Dedekind domains, and the corresponding extension `L/K` of fields of fractions is -assumed finite and Galois. Given `Q/P` a compatible pair of maximal ideals, under the -assumption that `A/P` is a finite field of size `q`, we construct an element `Frob_Q` -in `Gal(L/K)` and prove: - -1) `Frob_Q • Q = Q`; -2) `x ^ q ≡ Frob_Q x (mod Q)`. - -Examples where these hypotheses hold are: - -1) Finite Galois extensions of number fields and their integers or `S`-integers; -2) Finite Galois extensions of function fields over finite fields, and their `S`-integers for - `S` a nonempty set of places; -3) Finite Galois extensions of finite fields L/K where B/A=L/K and Q/P=0/0 (recovering the -classical theory of Frobenius elements) - -Note that if `Q` is ramified, there is more than one choice of `Frob_Q` which works; -for example if `L=ℚ(i)` and `K=ℚ` then both the identity and complex conjugation -work for `Frob Q` if `Q=(1+i)`, and `Frob` returns a random one (i.e. it's opaque; all we know -is that it satisfies the two properties). - -## The construction - -We follow a proof in a footnote of a book by Milne. **TODO** which book - -The Galois orbit of `Q` consists of `Q` and possibly some other primes `Q'`. The unit group -`(B/Q)ˣ` is finite and hence cyclic; so by the Chinese Remainder Theorem we may choose y ∈ B -which reduces to a generator mod Q and to 0 modulo all other Q' in the Galois orbit of Q. - -The polynomial `F = ∏ (X - σ y)`, the product running over `σ` in the Galois group, is in `B[X]` -and is Galois-stable so is in fact in `A[X]`. Hence if `Fbar` is `F mod Q` -then `Fbar` has coefficients in `A/P=𝔽_q` and thus `Fbar(y^q)=Fbar(y)^q=0`, meaning that `y^q` -is a root of `F` mod `Q` and thus congruent to `σ y mod Q` for some `σ`. We define `Frob Q` to -be this `σ`. - -## The proof - -We know `σ y ≡ y ^ q ≠ 0 mod Q`. Hence `σ y ∉ Q`, and thus `y ∉ σ⁻¹ Q`. But `y ∈ Q'` for all nontrivial -conjugates `Q'` of `Q`, hence `σ⁻¹ Q = Q` and thus `Q` is `σ`-stable. - -Hence `σ` induces a field automorphism of `B/Q` and we know it's `x ↦ x^q` on a generator, -so it's `x ↦ x^q` on everything. - -## Note - -This work started its life as Jou Glasheen's final project for Kevin Buzzard's -Formalising Mathematics 2024 course. - -## TODO - -Show that this applies to number fields and their rings of integers, -i.e. supply the finiteness typeclasses and descent hypothesis in this case. - --/ - -variable (A : Type*) [CommRing A] {B : Type*} [CommRing B] [Algebra A B] - -open scoped Pointwise - -variable {α : Type*} in -lemma Ideal.map_eq_comap_symm [Group α] [MulSemiringAction α B] (J : Ideal B) (σ : α) : - σ • J = J.comap (MulSemiringAction.toRingHom _ _ σ⁻¹) := - J.map_comap_of_equiv (MulSemiringAction.toRingEquiv α B σ) - -namespace ArithmeticFrobenius -/- - -## Auxiliary variables - -The noncomputable variables `g : (B ⧸ Q)ˣ` (a generator), -`y : B` (congruent to `g` mod `Q` and to `0` mod all Galois conjugates of `Q`, -`F : B[X]` (the product of `X - σ y` as `σ` runs through the Galois group), and -`m : A[X]`, the descent of `F` to `A[X]` (it's Galois-stable). --/ - -variable (Q : Ideal B) [Q.IsMaximal] - -variable [Fintype (B ⧸ Q)] - -noncomputable abbrev g : (B ⧸ Q)ˣ := (IsCyclic.exists_monoid_generator (α := (B ⧸ Q)ˣ)).choose - -lemma g_spec : ∀ (z : (B ⧸ Q)ˣ), z ∈ Submonoid.powers (g Q) := - (IsCyclic.exists_monoid_generator (α := (B ⧸ Q)ˣ)).choose_spec - -variable [Fintype (B ≃ₐ[A] B)] [DecidableEq (Ideal B)] - -/-- An element `y` of `B` exists, which is congruent to `b` mod `Q` -and to 0 mod all Galois conjugates of `Q` (if any).-/ -lemma exists_y : - ∃ y : B, (y : B ⧸ Q) = g Q ∧ ∀ Q' : Ideal B, Q' ∈ MulAction.orbit (B ≃ₐ[A] B) Q → Q' ≠ Q → y ∈ Q' := by - let O : Set (Ideal B) := MulAction.orbit (B ≃ₐ[A] B) Q - have hO' : Finite (O : Type _) := Set.finite_range _ - have hmax (I : O) : Ideal.IsMaximal (I : Ideal B) := by - rcases I with ⟨_, σ, rfl⟩ - convert Ideal.comap_isMaximal_of_surjective (K := Q) _ (AlgEquiv.surjective σ.symm) - apply Ideal.map_eq_comap_symm - have hPairwise : Pairwise fun (I : O) (J : O) ↦ IsCoprime (I : Ideal B) J := fun x y h ↦ ⟨1, 1, by - simp only [Ideal.one_eq_top, Ideal.top_mul] - exact Ideal.IsMaximal.coprime_of_ne (hmax x) (hmax y) <| mt Subtype.ext h⟩ - obtain ⟨y, hy⟩ := Ideal.exists_forall_sub_mem_ideal (ι := O) hPairwise - (fun J ↦ if J = ⟨Q, 1, by simp⟩ then (Ideal.Quotient.mk_surjective (g Q : B ⧸ Q)).choose else 0) - refine ⟨y, ?_, ?_⟩ - · specialize hy ⟨Q, 1, by simp⟩ - simp at hy - rw [← (Ideal.Quotient.mk_surjective (g Q : B ⧸ Q)).choose_spec] - exact - (Ideal.Quotient.mk_eq_mk_iff_sub_mem y - (Ideal.Quotient.mk_surjective (I := Q) (g Q)).choose).mpr hy - · rintro Q' ⟨σ, rfl⟩ hQ' - specialize hy ⟨σ • Q, σ, rfl⟩ - simp_all - -noncomputable abbrev y : B := - (exists_y A Q).choose - -lemma y_spec : ((y A Q : B) : B ⧸ Q) = g Q ∧ - ∀ Q' : Ideal B, Q' ∈ MulAction.orbit (B ≃ₐ[A] B) Q → Q' ≠ Q → (y A Q) ∈ Q' := - (exists_y A Q).choose_spec - -lemma y_mod_Q : Ideal.Quotient.mk Q (y A Q) = g Q := (y_spec A Q).1 - -lemma y_not_in_Q : (y A Q) ∉ Q := - mt Ideal.Quotient.eq_zero_iff_mem.mpr <| y_mod_Q A Q ▸ (g Q).ne_zero - -open Polynomial BigOperators - -/-- `F : B[X]` defined to be a product of linear factors `(X - τ • α)`; where -`τ` runs over `L ≃ₐ[K] L`, and `α : B` is an element which generates `(B ⧸ Q)ˣ` -and lies in `τ • Q` for all `τ ∉ (decomposition_subgroup_Ideal' A K L B Q)`.-/ -noncomputable abbrev F : B[X] := ∏ τ : B ≃ₐ[A] B, (X - C (τ • (y A Q))) - -lemma F_spec : F A Q = ∏ τ : B ≃ₐ[A] B, (X - C (τ • (y A Q))) := rfl - -variable {A Q} in -open Finset in -lemma F.smul_eq_self (σ : B ≃ₐ[A] B) : σ • (F A Q) = F A Q := calc - σ • F A Q = σ • ∏ τ : B ≃ₐ[A] B, (X - C (τ • (y A Q))) := by rw [F_spec] - _ = ∏ τ : B ≃ₐ[A] B, σ • (X - C (τ • (y A Q))) := smul_prod' - _ = ∏ τ : B ≃ₐ[A] B, (X - C ((σ * τ) • (y A Q))) := by simp [smul_sub] - _ = ∏ τ' : B ≃ₐ[A] B, (X - C (τ' • (y A Q))) := Fintype.prod_bijective (fun τ ↦ σ * τ) - (Group.mulLeft_bijective σ) _ _ (fun _ ↦ rfl) - _ = F A Q := by rw [F_spec] - -lemma F.y_eq_zero : (F A Q).eval (y A Q) = 0 := by - simp [F_spec, eval_prod, Finset.prod_eq_zero (Finset.mem_univ (1 : B ≃ₐ[A] B))] - -open scoped algebraMap - -noncomputable local instance : Algebra A[X] B[X] := - RingHom.toAlgebra (Polynomial.mapRingHom (Algebra.toRingHom)) - -omit [Fintype (B ≃ₐ[A] B)] [DecidableEq (Ideal B)] in -@[simp, norm_cast] -lemma coe_monomial (n : ℕ) (a : A) : ((monomial n a : A[X]) : B[X]) = monomial n (a : B) := - map_monomial _ - -lemma F.descent (h : ∀ b : B, (∀ σ : B ≃ₐ[A] B, σ • b = b) → ∃ a : A, b = a) : - ∃ m : A[X], (m : B[X]) = F A Q := by - choose f hf using h - classical - let f' : B → A := fun b ↦ if h : ∀ σ : B ≃ₐ[A] B, σ b = b then f b h else 37 - use (∑ x ∈ (F A Q).support, (monomial x) (f' ((F A Q).coeff x))) - ext N - push_cast - simp_rw [finset_sum_coeff, ← lcoeff_apply, lcoeff_apply, coeff_monomial] - simp only [Finset.sum_ite_eq', mem_support_iff, ne_eq, ite_not, f'] - symm - split - · next h => exact h - · next h1 => - rw [dif_pos <| fun σ ↦ ?_] - · refine hf ?_ ?_ - · nth_rw 2 [← F.smul_eq_self σ] - rfl - --- This will be true in applications to number fields etc. -variable (isGalois : ∀ b : B, (∀ σ : B ≃ₐ[A] B, σ • b = b) → ∃ a : A, b = a) - -noncomputable abbrev m := (F.descent A Q isGalois).choose - -lemma m_spec : ((m A Q isGalois) : B[X]) = F A Q := (F.descent A Q isGalois).choose_spec - -lemma m_spec' : (m A Q isGalois).map (algebraMap A B) = F A Q := by - rw [← m_spec A Q isGalois] - rfl - --- Amelia's trick to insert "let P be the ideal under Q" into the typeclass system -variable (P : Ideal A) [P.IsMaximal] [Algebra (A ⧸ P) (B ⧸ Q)] [IsScalarTower A (A⧸P) (B⧸Q)] - --- want to move from eval₂? -lemma m.mod_P_y_eq_zero : (m A Q isGalois).eval₂ (algebraMap A (B⧸Q)) (algebraMap B (B⧸Q) (y A Q)) = 0 := by - rw [show algebraMap A (B⧸Q) = (algebraMap B (B⧸Q)).comp (algebraMap A B) from IsScalarTower.algebraMap_eq A B (B ⧸ Q)] - rw [←eval₂_map] - change eval₂ _ _ (m A Q isGalois : B[X]) = _ - simp [m_spec A Q isGalois, eval_map, F.y_eq_zero] - -lemma m.y_mod_P_eq_zero : Polynomial.aeval (↑(y A Q) : B ⧸ Q) (m A Q isGalois) = 0 := by - rw [← aeval_map_algebraMap B, m_spec'] - -- why can't I do this with a `rw`? - change aeval (algebraMap B (B⧸Q) (y A Q)) _ = _ - rw [aeval_algebraMap_apply, coe_aeval_eq_eval, F.y_eq_zero A Q, map_zero] - - -noncomputable abbrev mmodP := (m A Q isGalois).map (algebraMap A (A⧸P)) - -open scoped Polynomial - --- lemma barg (K : Type*) [Field K] [Fintype K] : ∃ p n : ℕ, p.Prime ∧ Fintype.card K = p ^ n ∧ CharP K p := by --- obtain ⟨p, n, h₁, h₂⟩ := FiniteField.card' K --- refine ⟨p, n.val, h₁, h₂, ?_⟩ --- have : (p ^ n.val : K) = 0 := mod_cast h₂ ▸ Nat.cast_card_eq_zero K --- rw [CharP.charP_iff_prime_eq_zero h₁] --- simpa only [ne_eq, PNat.ne_zero, not_false_eq_true, pow_eq_zero_iff] using this - --- mathlib -lemma _root_.Polynomial.eval₂_pow_card (k : Type*) [Field k] [Fintype k] (f : k[X]) - (L : Type*) [CommRing L] [Algebra k L] - (t : L) : f.eval₂ (algebraMap k L) (t^(Fintype.card k)) = - (f.eval₂ (algebraMap k L) t)^(Fintype.card k) := by - simp_rw [← Polynomial.aeval_def] -- `eval₂ (algebraMap k L)` is just `aeval` - rw [← map_pow, ← FiniteField.expand_card, Polynomial.expand_aeval] - -variable [Fintype (A⧸P)] --- (m-bar)(y^q)=0 in B/Q -lemma m.mod_P_y_pow_q_eq_zero : - (m A Q isGalois).eval₂ (algebraMap A (B⧸Q)) ((algebraMap B (B⧸Q) (y A Q)) ^ (Fintype.card (A⧸P))) - = 0 := by - suffices ((m A Q isGalois).map (algebraMap A (A⧸P))).eval₂ (algebraMap (A⧸P) (B⧸Q)) - ((algebraMap B (B⧸Q) (y A Q)) ^ (Fintype.card (A⧸P))) = 0 by - rwa [eval₂_map, ← IsScalarTower.algebraMap_eq A (A ⧸ P) (B ⧸ Q)] at this - let foobar : Field (A⧸P) := ((Ideal.Quotient.maximal_ideal_iff_isField_quotient P).mp ‹_›).toField - rw [eval₂_pow_card, eval₂_map, ← IsScalarTower.algebraMap_eq A (A ⧸ P) (B ⧸ Q), m.mod_P_y_eq_zero, zero_pow] - exact Fintype.card_ne_zero - -lemma F.mod_Q_y_pow_q_eq_zero (isGalois : ∀ b : B, (∀ σ : B ≃ₐ[A] B, σ • b = b) → ∃ a : A, b = a) : (F A Q).eval₂ (algebraMap B (B⧸Q)) ((algebraMap B (B⧸Q) (y A Q)) ^ (Fintype.card (A⧸P))) = 0 := by - rw [← m_spec' A Q isGalois, eval₂_map]--, m.mod_P_y_pow_q_eq_zero] - rw [← IsScalarTower.algebraMap_eq A B (B ⧸ Q), m.mod_P_y_pow_q_eq_zero] - -lemma exists_Frob (isGalois : ∀ b : B, (∀ σ : B ≃ₐ[A] B, σ • b = b) → ∃ a : A, b = a) : ∃ σ : B ≃ₐ[A] B, σ (y A Q) - (y A Q) ^ (Fintype.card (A⧸P)) ∈ Q := by - have := F.mod_Q_y_pow_q_eq_zero A Q P isGalois - rw [F_spec, eval₂_finset_prod, Finset.prod_eq_zero_iff] at this - obtain ⟨σ, -, hσ⟩ := this - use σ - simp only [Ideal.Quotient.algebraMap_eq, AlgEquiv.smul_def, eval₂_sub, eval₂_X, eval₂_C, - sub_eq_zero] at hσ - exact (Submodule.Quotient.eq Q).mp (hσ.symm) - -noncomputable abbrev Frob := (exists_Frob A Q P isGalois).choose - -lemma Frob_spec : (Frob A Q isGalois P) • (y A Q) - (y A Q) ^ (Fintype.card (A⧸P)) ∈ Q := - (exists_Frob A Q P isGalois).choose_spec - -lemma Frob_Q : Frob A Q isGalois P • Q = Q := by - rw [smul_eq_iff_eq_inv_smul] - by_contra h - have hy : y A Q ∈ (Frob A Q isGalois P)⁻¹ • Q := (y_spec A Q).2 _ ⟨_, rfl⟩ (Ne.symm h) - have hy2 : (Frob A Q isGalois P) • (y A Q) ∈ Q := by - rwa [Ideal.map_eq_comap_symm] at hy - have this := Q.sub_mem hy2 <| Frob_spec A Q isGalois P - simp only [sub_sub_cancel] at this - exact y_not_in_Q A Q <| Ideal.IsPrime.mem_of_pow_mem (show Q.IsPrime by infer_instance) _ this diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean deleted file mode 100644 index d3c1e87a..00000000 --- a/FLT/MathlibExperiments/FrobeniusRiou.lean +++ /dev/null @@ -1,917 +0,0 @@ -/- -Copyright (c) 2024 Jou Glasheen. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jou Glasheen, Amelia Livingston, Jujian Zhang, Kevin Buzzard --/ -import Mathlib.FieldTheory.SeparableClosure -import Mathlib.RingTheory.Ideal.Over - -/-! - -# Frobenius elements. - -This file proves a general result in commutative algebra which can be used to define Frobenius -elements of Galois groups of local or fields (for example number fields). - -KB was alerted to this very general result (which needs no Noetherian or finiteness assumptions -on the rings, just on the Galois group) by Joël Riou -here https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Uses.20of.20Frobenius.20elements.20in.20mathematics/near/448934112 - -## Mathematical details - -### The general commutative algebra result - -This is Theorem 2 in Chapter V, Section 2, number 2 of Bourbaki Alg Comm. It says the following. -Let `A → B` be commutative rings and let `G` be a finite group acting on `B` by ring automorphisms, -such that the `G`-invariants of `B` are exactly the image of `A`. - -The two claims of the theorem are: -(i) If `P` is a prime ideal of `A` then `G` acts transitively on the primes of `B` above `P`. -(ii) If `Q` is a prime ideal of `B` lying over `P` then the canonica map from the stabilizer of `Q` -in `G` to the automorphism group of the residue field extension `Frac(B/Q) / Frac(A/P)` is -surjective. - -We say "automorphism group" rather than "Galois group" because the extension might not be -separable (it is algebraic and normal however, but it can be infinite; however its maximal -separable subextension is finite). - -This result means that if the inertia group I_Q is trivial and the residue fields are finite, -there's a Frobenius element Frob_Q in the stabiliser of Q, and a Frobenius conjugacy class -Frob_P in G. - --/ - - -variable {A : Type*} [CommRing A] - {B : Type*} [CommRing B] [Algebra A B] --[Algebra.IsIntegral A B] - {G : Type*} [Group G] [Finite G] [MulSemiringAction G B] - - - -open scoped algebraMap - ---variable (hFull : ∀ (b : B), (∀ (g : G), g • b = b) ↔ ∃ a : A, b = a) ---variable (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) - -section misc - -variable {A : Type*} [CommRing A] - {B : Type*} [CommRing B] [Algebra A B] - {G : Type*} [Group G] [MulSemiringAction G B] - [SMulCommClass G A B] - -open scoped Pointwise - -/- -If you're happy to stick to finite G, it's just this: - -private theorem norm_fixed' (b : B) (g : G) [Finite G] : g • (∏ᶠ σ : G, σ • b) = ∏ᶠ σ : G, σ • b := calc - g • (∏ᶠ σ : G, σ • b) = ∏ᶠ σ : G, g • (σ • b) := smul_finprod' _ - _ = ∏ᶠ σ : G, σ • b := finprod_eq_of_bijective (g • ·) (MulAction.bijective g) - fun x ↦ smul_smul g x b - -But the below proof works in general. --/ - -private theorem norm_fixed (b : B) (g : G) : g • (∏ᶠ σ : G, σ • b) = ∏ᶠ σ : G, σ • b := by - obtain (hfin | hinf) := em <| Finite G - · calc - g • (∏ᶠ σ : G, σ • b) = ∏ᶠ σ : G, g • (σ • b) := smul_finprod' _ - _ = ∏ᶠ σ : G, σ • b := finprod_eq_of_bijective (g • ·) (MulAction.bijective g) - fun x ↦ smul_smul g x b - · obtain (rfl | hb) := eq_or_ne b 1 - · simp - · suffices (Function.mulSupport ((· • b) : G → B)).Infinite by - classical - simp [finprod_def, dif_neg this] - have htop : (⊤ : Set G).Infinite := by simpa using Set.infinite_univ_iff.mpr ({ not_finite := hinf }) - convert htop - rw [eq_top_iff] - intro g _ - simp only [Function.mem_mulSupport] - contrapose! hb - apply_fun (fun x ↦ g⁻¹ • x) at hb - simpa using hb - -theorem _root_.Ideal.IsPrime.finprod_mem_iff_exists_mem {R S : Type*} [Finite R] [CommSemiring S] - (I : Ideal S) [hI : I.IsPrime] (f : R → S) : - ∏ᶠ x, f x ∈ I ↔ ∃ p, f p ∈ I := by - have := Fintype.ofFinite R - rw [finprod_eq_prod_of_fintype, Finset.prod_eq_multiset_prod, hI.multiset_prod_mem_iff_exists_mem] - simp - -end misc - -section charpoly - -open Polynomial BigOperators - -variable {A : Type*} [CommRing A] - {B : Type*} [CommRing B] [Algebra A B] - {G : Type*} [Group G] [MulSemiringAction G B] --[SMulCommClass G A B] - - -variable (G) in -/-- The characteristic polynomial of an element `b` of a `G`-semiring `B` -is the polynomial `∏_{g ∈ G} (X - g • b)` (here `G` is finite; junk -returned in the infinite case) .-/ -noncomputable def MulSemiringAction.CharacteristicPolynomial.F (b : B) : B[X] := - ∏ᶠ τ : G, (X - C (τ • b)) - -namespace MulSemiringAction.CharacteristicPolynomial - -theorem F_spec (b : B) : F G b = ∏ᶠ τ : G, (X - C (τ • b)) := rfl - -section F_API - -variable [Finite G] - -theorem F_monic [Nontrivial B] (b : B) : (F G b).Monic := by - have := Fintype.ofFinite G - rw [Monic, F_spec, finprod_eq_prod_of_fintype, leadingCoeff_prod'] <;> simp - -theorem F_natdegree [Nontrivial B] (b : B) : (F G b).natDegree = Nat.card G := by - have := Fintype.ofFinite G - rw [F_spec, finprod_eq_prod_of_fintype, natDegree_prod_of_monic _ _ (fun _ _ => monic_X_sub_C _)] - simp only [natDegree_X_sub_C, Finset.sum_const, Finset.card_univ, Fintype.card_eq_nat_card, - nsmul_eq_mul, mul_one, Nat.cast_id] - -variable (G) in -theorem F_degree [Nontrivial B] (b : B) : (F G b).degree = Nat.card G := by - have := Fintype.ofFinite G - rw [degree_eq_iff_natDegree_eq_of_pos Nat.card_pos, F_natdegree] - -theorem F_smul_eq_self (σ : G) (b : B) : σ • (F G b) = F G b := calc - σ • F G b = σ • ∏ᶠ τ : G, (X - C (τ • b)) := by rw [F_spec] - _ = ∏ᶠ τ : G, σ • (X - C (τ • b)) := smul_finprod' _ - _ = ∏ᶠ τ : G, (X - C ((σ * τ) • b)) := by simp [smul_sub, smul_smul] - _ = ∏ᶠ τ' : G, (X - C (τ' • b)) := finprod_eq_of_bijective (fun τ ↦ σ * τ) - (Group.mulLeft_bijective σ) (fun _ ↦ rfl) - _ = F G b := by rw [F_spec] - -theorem F_eval_eq_zero (b : B) : (F G b).eval b = 0 := by - let foo := Fintype.ofFinite G - simp [F_spec,finprod_eq_prod_of_fintype,eval_prod] - apply @Finset.prod_eq_zero _ _ _ _ _ (1 : G) (Finset.mem_univ 1) - simp - -private theorem F_coeff_fixed (b : B) (n : ℕ) (g : G) : - g • (F G b).coeff n = (F G b).coeff n := by - change (g • (F G b)).coeff n = _ - rw [F_smul_eq_self] - -end F_API - -open scoped algebraMap - -noncomputable local instance : Algebra A[X] B[X] := - RingHom.toAlgebra (Polynomial.mapRingHom (Algebra.toRingHom)) - -@[simp, norm_cast] -theorem _root_.coe_monomial (n : ℕ) (a : A) : ((monomial n a : A[X]) : B[X]) = monomial n (a : B) := - map_monomial _ - -section full_descent - -variable (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) - --- Remark: the `splitting_of_full` approach is lousy and should be --- replaced by the commented-out code below (lines 275-296 currently) - -/-- This "splitting" function from B to A will only ever be evaluated on -G-invariant elements of B, and the two key facts about it are -that it lifts such an element to `A`, and for reasons of -convenience it lifts `1` to `1`. -/ -noncomputable def splitting_of_full - (b : B) : A := by classical - exact - if b = 1 then 1 else - if h : ∀ σ : G, σ • b = b then (hFull b h).choose - else 37 - -theorem splitting_of_full_spec {b : B} (hb : ∀ σ : G, σ • b = b) : - splitting_of_full hFull b = b := by - unfold splitting_of_full - split_ifs with h1 - · rw_mod_cast [h1] - · exact (hFull b hb).choose_spec.symm - -theorem splitting_of_full_one : splitting_of_full hFull 1 = 1 := by - unfold splitting_of_full - rw [if_pos rfl] - -noncomputable def M (b : B) : A[X] := - (∑ x ∈ (F G b).support, monomial x (splitting_of_full hFull ((F G b).coeff x))) - -theorem M_deg_le (b : B) : (M hFull b).degree ≤ (F G b).degree := by - unfold M - have := Polynomial.degree_sum_le (F G b).support (fun x => monomial x (splitting_of_full hFull ((F G b).coeff x))) - refine le_trans this ?_ - rw [Finset.sup_le_iff] - intro n hn - apply le_trans (degree_monomial_le n _) ?_ - exact le_degree_of_mem_supp n hn - -variable [Nontrivial B] [Finite G] - -theorem M_coeff_card (b : B) : - (M hFull b).coeff (Nat.card G) = 1 := by - unfold M - simp only [finset_sum_coeff] - have hdeg := F_degree G b - rw [degree_eq_iff_natDegree_eq_of_pos Nat.card_pos] at hdeg - rw [ ← hdeg] - rw [Finset.sum_eq_single_of_mem ((F G b).natDegree)] - · have : (F G b).Monic := F_monic b - simp - simp_all [splitting_of_full_one] - · refine natDegree_mem_support_of_nonzero ?h.H - intro h - rw [h] at hdeg - have : 0 < Nat.card G := Nat.card_pos - simp_all - · intro d _ hd - exact coeff_monomial_of_ne (splitting_of_full hFull ((F G b).coeff d)) hd - -theorem M_deg_eq_F_deg [Nontrivial A] (b : B) : (M hFull b).degree = (F G b).degree := by - apply le_antisymm (M_deg_le hFull b) - rw [F_degree] - have := M_coeff_card hFull b - refine le_degree_of_ne_zero ?h - rw [this] - exact one_ne_zero - -theorem M_deg [Nontrivial A] (b : B) : (M hFull b).degree = Nat.card G := by - rw [M_deg_eq_F_deg hFull b] - exact F_degree G b - -theorem M_monic (b : B) : (M hFull b).Monic := by - have this1 := M_deg_le hFull b - have this2 := M_coeff_card hFull b - have this3 : 0 < Nat.card G := Nat.card_pos - rw [← F_natdegree b] at this2 this3 - -- then the hypos say deg(M)<=n, coefficient of X^n is 1 in M - have this4 : (M hFull b).natDegree ≤ (F G b).natDegree := natDegree_le_natDegree this1 - exact Polynomial.monic_of_natDegree_le_of_coeff_eq_one _ this4 this2 - -omit [Nontrivial B] in -theorem M_spec (b : B) : ((M hFull b : A[X]) : B[X]) = F G b := by - unfold M - ext N - push_cast - simp_rw [splitting_of_full_spec hFull <| F_coeff_fixed b _] - simp_rw [finset_sum_coeff, ← lcoeff_apply, lcoeff_apply, coeff_monomial] - aesop - -omit [Nontrivial B] in -theorem M_spec_map (b : B) : (map (algebraMap A B) (M hFull b)) = F G b := by - rw [← M_spec hFull b]; rfl - -omit [Nontrivial B] in -theorem M_eval_eq_zero (b : B) : (M hFull b).eval₂ (algebraMap A B) b = 0 := by - rw [eval₂_eq_eval_map, M_spec_map, F_eval_eq_zero] - -include hFull in -theorem isIntegral : Algebra.IsIntegral A B where - isIntegral b := ⟨M hFull b, M_monic hFull b, M_eval_eq_zero hFull b⟩ - -end full_descent - -end MulSemiringAction.CharacteristicPolynomial - -end charpoly - -section part_a - -open MulSemiringAction.CharacteristicPolynomial - -variable {A : Type*} [CommRing A] - {B : Type*} [CommRing B] [Algebra A B] [Nontrivial B] - {G : Type*} [Group G] [Finite G] [MulSemiringAction G B] - -theorem isIntegral_of_Full (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) : - Algebra.IsIntegral A B where - isIntegral b := ⟨M hFull b, M_monic hFull b, M_eval_eq_zero hFull b⟩ - -variable (P Q : Ideal B) [P.IsPrime] [Q.IsPrime] - (hPQ : Ideal.comap (algebraMap A B) P = Ideal.comap (algebraMap A B) Q) - -open scoped Pointwise - -theorem Nontrivial_of_exists_prime {R : Type*} [CommRing R] - (h : ∃ P : Ideal R, P.IsPrime) : Nontrivial R := by - contrapose! h - intro P hP - rw [@not_nontrivial_iff_subsingleton] at h - obtain ⟨h, _⟩ := hP - apply h - apply Subsingleton.elim - --- (Part a of Théorème 2 in section 2 of chapter 5 of Bourbaki Alg Comm) -omit [Nontrivial B] in -theorem part_a [SMulCommClass G A B] - (hPQ : Ideal.comap (algebraMap A B) P = Ideal.comap (algebraMap A B) Q) - (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) : - ∃ g : G, Q = g • P := by - haveI : Nontrivial B := Nontrivial_of_exists_prime ⟨Q, inferInstance⟩ - haveI : Algebra.IsIntegral A B := isIntegral_of_Full hFull' - cases nonempty_fintype G - suffices ∃ g : G, Q ≤ g • P by - obtain ⟨g, hg⟩ := this - use g - by_contra! hQ - have : Q < g • P := lt_of_le_of_ne hg hQ - obtain ⟨x, hxP, hxQ⟩ := Set.exists_of_ssubset <| this - apply (Ideal.comap_lt_comap_of_integral_mem_sdiff (R := A) hg ⟨hxP, hxQ⟩ <| - Algebra.isIntegral_def.1 inferInstance x).ne - rw [← hPQ] - ext x - specialize hFull' (algebraMap A B x) - have : ∀ (g : G), g • (algebraMap A B x) = (algebraMap A B x) := fun g ↦ by - rw [Algebra.algebraMap_eq_smul_one, smul_comm, smul_one] - simp only [Ideal.mem_comap] - nth_rw 2 [← this] - exact Ideal.smul_mem_pointwise_smul_iff.symm - suffices ∃ g ∈ (⊤ : Finset G), Q ≤ g • P by - convert this; simp - rw [← Ideal.subset_union_prime 1 1 <| fun g _ _ _ ↦ ?_]; swap - · exact Ideal.map_isPrime_of_equiv (MulSemiringAction.toRingEquiv _ _ g) - intro x hx - specialize hFull' (∏ᶠ σ : G, σ • x) - obtain ⟨a, ha⟩ := hFull' (norm_fixed _) - have : (a : B) ∈ Q := by - rw [← ha, Ideal.IsPrime.finprod_mem_iff_exists_mem] - use 1 - simpa using hx - have : (a : B) ∈ P := by - unfold Algebra.cast - rwa [← Ideal.mem_comap, hPQ, Ideal.mem_comap] - rw [← ha, Ideal.IsPrime.finprod_mem_iff_exists_mem] at this - obtain ⟨σ, hσ⟩ : ∃ σ : G, σ • x ∈ P := this - simp only [Finset.top_eq_univ, Finset.coe_univ, Set.mem_univ, Set.iUnion_true, Set.mem_iUnion, - SetLike.mem_coe] - use σ⁻¹ - rwa [Ideal.mem_inv_pointwise_smul_iff] - -end part_a - --- section normal_elements --- I'm going to avoid this because I'm just going to use scaling. --- I'll show that every nonzero element of B/Q divides an element of A/P. - --- variable (K : Type*) [Field K] {L : Type*} [Field L] [Algebra K L] - --- open Polynomial - --- I've commented out the next section because ACL suggested --- reading up-to-date Bourbaki here https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/poly.20whose.20roots.20are.20the.20products.20of.20the.20roots.20of.20polys/near/468585267 --- and apparently this will avoid the def below. - --- def IsNormalElement (x : L) : Prop := Splits (algebraMap K L) (minpoly K x) - --- namespace IsNormalElement - --- theorem iff_exists_monic_splits {x : L} (hx : IsIntegral K x) : --- IsNormalElement K x ↔ --- ∃ P : K[X], P.Monic ∧ P.eval₂ (algebraMap K L) x = 0 ∧ Splits (algebraMap K L) P := by --- constructor --- · intro h --- exact ⟨minpoly K x, minpoly.monic hx, minpoly.aeval K x, h⟩ --- · rintro ⟨P, hPmonic, hPeval, hPsplits⟩ --- -- need min poly divides P and then it should all be over --- sorry -- presumably some form of this is in the library - --- theorem prod {x y : L} (hxint : IsIntegral K x) (hyint : IsIntegral K y) --- (hx : IsNormalElement K x) (hy : IsNormalElement K y) : --- IsNormalElement K (x * y) := by --- rw [iff_exists_monic_splits K hxint] at hx --- obtain ⟨Px, hx1, hx2, hx3⟩ := hx --- rw [iff_exists_monic_splits K hyint] at hy --- obtain ⟨Py, hy1, hy2, hy3⟩ := hy --- rw [iff_exists_monic_splits K <| IsIntegral.mul hxint hyint] --- -- If roots of Px are xᵢ and roots of Py are yⱼ, then use the poly whose roots are xᵢyⱼ. --- -- Do we have this? --- -- Is this even the best way to go about this? --- -- Note: Chambert-Loir says there's a proof in Bourbaki --- sorry - --- -- API - --- end IsNormalElement - --- end normal_elements - -section part_b - -variable {A : Type*} [CommRing A] - {B : Type*} [CommRing B] [Algebra A B] - {G : Type*} [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B] - -/- -Set-up for part (b) of the lemma. G acts on B with invariants A (or more precisely the -image of A). Warning: `P` was a prime ideal of `B` in part (a) but it's a prime ideal -of `A` here, in fact it's `Q ∩ A`, the preimage of `Q` in `A`. - -We want to consider the following commutative diagram. - -B ---> B / Q -----> L = Frac(B/Q) -/\ /\ /\ -| | | -| | | -A ---> A / P ----> K = Frac(A/P) - -We will get to L, K, and the second square later. -First let's explain how to do P and Q. --/ -variable (Q : Ideal B) [Q.IsPrime] (P : Ideal A) [P.IsPrime] --- #synth Algebra A (B ⧸ Q) #exit -- works ----synth IsScalarTower A B (B ⧸ Q) #exit-- works --- (hPQ : Ideal.comap (algebraMap A B) P = p) -- we will *prove* this from the --- commutativity of the diagram! This is a trick I learnt from Jou who apparently --- learnt it from Amelia - [Algebra (A ⧸ P) (B ⧸ Q)] [IsScalarTower A (A ⧸ P) (B ⧸ Q)] --- So now we know the left square commutes. --- Amelia's first trick: commutativity of th LH diagram implies `P ⊆ Q ∩ A` --- For the map `A -> A/P -> B/Q` must equal the map `A -> B -> B/Q` so `P` must --- be a subset of the kernel of `A → B/Q`, which is `A ∩ Q` - -omit [P.IsPrime] in -theorem Ideal.Quotient.eq_zero_iff_mem' (x : A) : - algebraMap A (A ⧸ P) x = 0 ↔ x ∈ P := - Ideal.Quotient.eq_zero_iff_mem - -section B_mod_Q_over_A_mod_P_stuff - -section Mathlib.RingTheory.Ideal.Quotient - -namespace Ideal - -variable {R : Type*} [CommRing R] {I : Ideal R} - -protected noncomputable -def Quotient.out (x : R ⧸ I) := x.out - -theorem Quotient.out_eq (x : R ⧸ I) : Ideal.Quotient.mk I (Ideal.Quotient.out x) = x := by - simp only [Ideal.Quotient.out, Ideal.Quotient.mk, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, - Submodule.Quotient.mk, Quotient.out_eq'] - -@[elab_as_elim] -protected theorem Quotient.induction_on - {p : R ⧸ I → Prop} (x : R ⧸ I) (h : ∀ a, p (Ideal.Quotient.mk I a)) : p x := - Quotient.inductionOn x h - -end Ideal - -end Mathlib.RingTheory.Ideal.Quotient - -namespace MulSemiringAction.CharacteristicPolynomial - - -open Polynomial -/- -I didn't check that this definition was independent -of the lift `b` of `bbar` (and it might not even be true). -But this doesn't matter, because `G` no longer acts on `B/Q`. -All we need is that `Mbar` is monic of degree `|G|`, is defined over the bottom ring -and kills `bbar`. --/ -variable {Q} in -noncomputable def Mbar - (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) - (bbar : B ⧸ Q) : (A ⧸ P)[X] := - Polynomial.map (Ideal.Quotient.mk P) <| M hFull' <| Ideal.Quotient.out bbar - -variable (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) - -omit [SMulCommClass G A B] [Q.IsPrime] [P.IsPrime] [Algebra (A ⧸ P) (B ⧸ Q)] - [IsScalarTower A (A ⧸ P) (B ⧸ Q)] in -theorem Mbar_monic [Nontrivial B] (bbar : B ⧸ Q) : (Mbar P hFull' bbar).Monic := by - have := M_monic hFull' - simp [Mbar, (M_monic hFull' _).map] - -omit [SMulCommClass G A B] [Q.IsPrime] [Algebra (A ⧸ P) (B ⧸ Q)] [IsScalarTower A (A ⧸ P) (B ⧸ Q)] in -theorem Mbar_deg [Nontrivial A] [Nontrivial B] (bbar : B ⧸ Q) : - degree (Mbar P hFull' bbar) = Nat.card G := by - simp only [Mbar] - rw [degree_map_eq_of_leadingCoeff_ne_zero] - · exact M_deg hFull' _ - · rw [(M_monic hFull' _).leadingCoeff] - simp only [map_one, ne_eq, one_ne_zero, not_false_eq_true] - -omit [SMulCommClass G A B] [Q.IsPrime] [P.IsPrime] in -theorem Mbar_eval_eq_zero [Nontrivial A] [Nontrivial B] (bbar : B ⧸ Q) : - eval₂ (algebraMap (A ⧸ P) (B ⧸ Q)) bbar (Mbar P hFull' bbar) = 0 := by - have h := congr_arg (algebraMap B (B ⧸ Q)) (M_eval_eq_zero hFull' (Ideal.Quotient.out bbar)) - rw [map_zero, hom_eval₂, Ideal.Quotient.algebraMap_eq, Ideal.Quotient.out_eq] at h - simpa [Mbar, eval₂_map, ← Ideal.Quotient.algebraMap_eq, - ← IsScalarTower.algebraMap_eq A (A ⧸ P) (B ⧸ Q), IsScalarTower.algebraMap_eq A B (B ⧸ Q)] - -end CharacteristicPolynomial - -open CharacteristicPolynomial in -omit [SMulCommClass G A B] [Q.IsPrime] [P.IsPrime] in -theorem reduction_isIntegral - [Nontrivial A] [Nontrivial B] - (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) : - Algebra.IsIntegral (A ⧸ P) (B ⧸ Q) where - isIntegral x := ⟨Mbar P hFull' x, Mbar_monic Q P hFull' x, Mbar_eval_eq_zero Q P hFull' x⟩ - -end MulSemiringAction - -theorem Polynomial.nonzero_const_if_isIntegral (R S : Type) [CommRing R] [Nontrivial R] - [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) : - ∃ (q : Polynomial R), q.coeff 0 ≠ 0 ∧ q.eval₂ (algebraMap R S) s = 0 := by - obtain ⟨p, p_monic, p_eval⟩ := (@Algebra.isIntegral_def R S).mp inferInstance s - have p_nzero := ne_zero_of_ne_zero_of_monic X_ne_zero p_monic - obtain ⟨q, p_eq, q_ndvd⟩ := Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd p p_nzero 0 - rw [C_0, sub_zero] at p_eq - rw [C_0, sub_zero] at q_ndvd - use q - constructor - . intro q_coeff_0 - exact q_ndvd <| X_dvd_iff.mpr q_coeff_0 - . rw [p_eq, eval₂_mul] at p_eval - rcases NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero p_eval with Xpow_eval | q_eval - . by_contra - apply hs - rw [eval₂_X_pow] at Xpow_eval - exact pow_eq_zero Xpow_eval - . exact q_eval - -theorem Algebra.exists_dvd_nonzero_if_isIntegral (R S : Type) [CommRing R] [Nontrivial R] - [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) : - ∃ r : R, r ≠ 0 ∧ s ∣ (algebraMap R S) r := by - obtain ⟨q, q_zero_coeff, q_eval_zero⟩ := Polynomial.nonzero_const_if_isIntegral R S s hs - use q.coeff 0 - refine ⟨q_zero_coeff, ?_⟩ - rw [← Polynomial.eval₂_X (algebraMap R S) s, ← dvd_neg, ← Polynomial.eval₂_C (algebraMap R S) s] - rw [← zero_add (-_), Mathlib.Tactic.RingNF.add_neg, ← q_eval_zero, ← Polynomial.eval₂_sub] - apply Polynomial.eval₂_dvd - exact Polynomial.X_dvd_sub_C - -end B_mod_Q_over_A_mod_P_stuff - -/- -\section{The extension $L/K$.} - -\begin{theorem} - \label{foo1} -If $\lambda\in L$ then there's a monic polynomial $P_\lambda\in K[X]$ of degree $|G|$ -with $\lambda$ as a root, and which splits completely in $L[X]$. -\end{theorem} -\begin{proof} - A general $\lambda\in L$ can be written as $\beta_1/\beta_2$ where $\beta_1,\beta_2\in B/Q$. - The previous corollary showed that there's some nonzero $\alpha\in A/P$ such that $\beta_2$ - divides $\alpha$, and hence $\alpha\lambda\in B/Q$ (we just cleared denominators). - Thus $\alpha\lambda$ is a root of some monic polynomial $f(x)\in (A/P)[X]$, - by~\ref{MulSemiringAction.CharacteristicPolynomial.Mbar_eval_eq_zero}. - The polynomial $f(\alpha x)\in (A/P)[X]$ thus - has $\lambda$ as a root, but it is not monic; its leading term is $\alpha^n$. - Dividing through in $K[X]$ gives us the polynomial we seek. -\end{proof} - -\begin{corollary} The extension $L/K$ is algebraic and normal. -\end{corollary} -\begin{proof} \uses{foo1} - Exercise using the previous theorem. -\end{proof} - -Note that $L/K$ might not be separable and might have infinite degree. However - -\begin{corollary} Any subextension of $L/K$ which is finite and separable over $K$ - has degree at most $|G|$. -\end{corollary} -\begin{proof} - Finite and separable implies simple, and we've already seen that any - element of $L$ has degree at most $|G|$ over $K$. -\end{proof} - -\begin{corollary} The maximal separable subextension $M$ of $L/K$ has degree at most $|G|$. -\end{corollary} -\begin{proof} If it has dimension greater than $|G|$ over $K$, then it has a finitely-generated - subfeld of $K$-dimension greater than $|G|$, and is finite and separable, contradicting - the previous result. -\end{proof} - -\begin{corollary} $\Aut_K(L)$ is finite. -\end{corollary} -\begin{proof} Any $K$-automorphism of $L$ is determined by where it sends $M$. -\end{proof} - -\begin{corollary} $\Aut_{A/P}(B/Q)$ is finite. -\end{corollary} -\begin{proof} - Two elements of $\Aut_{A/P}(B/Q)$ which agree once extended to automorphisms of $L$ - must have already been equal, as $B/Q\subseteq L$. Hence the canonical map - from $\Aut_{A/P}(B/Q)$ to $\Aut_K(L)$ is injective. -\end{proof} - -\section{Proof of surjectivity.} - -\begin{definition} We fix once and for all some nonzero $y\in B/Q$ such that $M=K(y)$, - with $M$ the maximal separable subextension of $L/K$. -\end{definition} - -Note that the existence of some $\lambda\in L$ with this property just comes from finite -and separable implies simple; we can use the ``clear denominator'' technique introduced -earlier to scale this by some nonzero $\alpha\in A$ into $B/Q$, as -$K(\lambda)=K(\alpha\lambda)$. - -Here is a slightly delicate result whose proof I haven't thought too hard about. -\begin{theorem} There exists some $x\in B$ and $\alpha\in A$ with the following - properties. - \begin{enumerate} - \item $x=\alpha y$ mod $Q$ and $\alpha$ isn't zero mod $Q$. - \item $x\in Q'$ for all $Q'\not=Q$ in the $G$-orbit of $Q$. - \end{enumerate} -\end{theorem} -\begin{proof} - Idea. Localise away from P, then all the $Q_i$ are maximal, use CRT and then clear denominators. -\end{proof} - -We now choose some $x\in B[1/S]$ which is $y$ modulo $Q$ and $0$ modulo all the other -primes of $B$ above $P$, and consider the monic degree $|G|$ polynomial $f$ in $K[X]$ -with $x$ and its conjugates as roots. If $\sigma\in\Aut_K(L)$ then $\sigma(\overline{x})$ -is a root of $f$ as $\sigma$ fixes $K$ pointwise. Hence $\sigma(\overline{x})=\overline{g(x)}$ -for some $g\in G$, and because $\sigma(\overline{x})\not=0$ we have $\overline{g(x)}\not=0$ -and hence $g(x)\notin Q[1/S]$. Hence $x\notin g^{-1} Q[1/S]$ and thus $g^{-1}Q=Q$ and $g\in SD_Q$. -Finally we have $\phi_g=\sigma$ on $K$ and on $y$, so they are equal on $M$ and hence on $L$ as -$L/M$ is purely inseparable. - -This part of the argument seems weak. --/ - -section L_over_K_stuff - --- Let's now make the right square. First `L` -variable (L : Type*) [Field L] [Algebra (B ⧸ Q) L] [IsFractionRing (B ⧸ Q) L] - -- Now top left triangle: A / P → B / Q → L commutes - [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] - -- now introduce K - (K : Type*) [Field K] [Algebra (A ⧸ P) K] [IsFractionRing (A ⧸ P) K] - -- now make bottom triangle commute - [Algebra K L] [IsScalarTower (A ⧸ P) K L] - -- So now both squares commute. - --- do I need this? --- [Algebra A K] [IsScalarTower A (A ⧸ P) K] - --- Do I need this: --- [Algebra B L] [IsScalarTower B (B ⧸ Q) L] - -variable [Nontrivial B] - - --- Do we need a version of Ideal.Quotient.eq_zero_iff_mem with algebraMap? - - --- not sure if we need this but let's prove it just to check our setup is OK. --- The claim is that the preimage of Q really is P (rather than just containing P) --- and the proof is that A/P -> B/Q extends to a map of fields which is injective, --- so A/P -> B/Q must also be injective. -open IsScalarTower in -example : Ideal.comap (algebraMap A B) Q = P := by - ext x - simp only [Ideal.mem_comap] - rw [← Ideal.Quotient.eq_zero_iff_mem', ← Ideal.Quotient.eq_zero_iff_mem'] - rw [← map_eq_zero_iff _ <| IsFractionRing.injective (A ⧸ P) K] - rw [← map_eq_zero_iff _ <| IsFractionRing.injective (B ⧸ Q) L] - rw [← map_eq_zero_iff _ <| RingHom.injective ((algebraMap K L) : K →+* L)] - rw [← algebraMap_apply A B (B ⧸ Q)] - rw [← algebraMap_apply (A ⧸ P) K L] - rw [algebraMap_apply A (A ⧸ P) (B ⧸ Q)] - rw [algebraMap_apply (A ⧸ P) (B ⧸ Q) L] - -open Polynomial BigOperators - -open scoped algebraMap - -noncomputable local instance : Algebra A[X] B[X] := - RingHom.toAlgebra (Polynomial.mapRingHom (Algebra.toRingHom)) - -theorem IsAlgebraic.invLoc {R S K : Type*} [CommRing R] {M : Submonoid R} [CommRing S] [Algebra R S] - [IsLocalization M S] {x : M} [CommRing K] [Algebra K S] (h : IsAlgebraic K ((x : R) : S)): - IsAlgebraic K (IsLocalization.mk' S 1 x) := by - rw [← IsAlgebraic.invOf_iff, IsLocalization.invertible_mk'_one_invOf] - exact h - -open MulSemiringAction.CharacteristicPolynomial - -namespace Bourbaki52222 - -variable (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) in -variable (G) in -noncomputable def residueFieldExtensionPolynomial [DecidableEq L] (x : L) : K[X] := - if x = 0 then monomial (Nat.card G) 1 - else 37 -- this is not actually right. In the nonzero case you - -- clear denominators with a nonzero element of A, using - -- `Algebra.exists_dvd_nonzero_if_isIntegral` above, and then use Mbar - -- scaled appropriately. - -theorem f_exists [DecidableEq L] (l : L) : - ∃ f : K[X], f.Monic ∧ f.degree = Nat.card G ∧ - eval₂ (algebraMap K L) l f = 0 ∧ f.Splits (algebraMap K L) := by - use Bourbaki52222.residueFieldExtensionPolynomial G L K l - sorry - -theorem algebraMap_cast {R S: Type*} [CommRing R] [CommRing S] [Algebra R S] (r : R) : - (r : S) = (algebraMap R S) r := by - rfl - -theorem algebraMap_algebraMap {R S T : Type*} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] - [Algebra S T] [Algebra R T] [IsScalarTower R S T] (r : R) : - (algebraMap S T) ((algebraMap R S) r) = (algebraMap R T) r := by - exact Eq.symm (IsScalarTower.algebraMap_apply R S T r) - -theorem Algebra.isAlgebraic_of_subring_isAlgebraic {R k K : Type*} [CommRing R] [CommRing k] - [CommRing K] [Algebra R K] [IsFractionRing R K] [Algebra k K] [NoZeroDivisors k] - (h : ∀ x : R, IsAlgebraic k (x : K)) : Algebra.IsAlgebraic k K := by - rw [Algebra.isAlgebraic_def] - let M := nonZeroDivisors R - intro x - have ⟨r, s, h'⟩ := IsLocalization.mk'_surjective M x - have : x = r * IsLocalization.mk' K 1 s := by - rw [← h', IsLocalization.mul_mk'_eq_mk'_of_mul] - simp - rw [this] - apply IsAlgebraic.mul (h r) - exact IsAlgebraic.invLoc (h s) - --- this uses `Algebra.isAlgebraic_of_subring_isAlgebraic` but I think we're going to have --- to introduce `f` anyway because we need not just that the extension is algebraic but --- that every element satisfies a poly of degree <= |G|. -theorem algebraic {A : Type*} [CommRing A] {B : Type*} [Nontrivial B] [CommRing B] [Algebra A B] - [Algebra.IsIntegral A B] {G : Type*} [Group G] [Finite G] [MulSemiringAction G B] (Q : Ideal B) - [Q.IsPrime] (P : Ideal A) [P.IsPrime] [Algebra (A ⧸ P) (B ⧸ Q)] - [IsScalarTower A (A ⧸ P) (B ⧸ Q)] (L : Type*) [Field L] [Algebra (B ⧸ Q) L] - [IsFractionRing (B ⧸ Q) L] [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] - (K : Type*) [Field K] [Algebra (A ⧸ P) K] [IsFractionRing (A ⧸ P) K] - [Algebra K L] [IsScalarTower (A ⧸ P) K L] [Algebra A K] [IsScalarTower A (A ⧸ P) K] - [Algebra B L] [IsScalarTower B (B ⧸ Q) L] [Algebra A L] [IsScalarTower A K L] - [IsScalarTower A B L] - (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a): Algebra.IsAlgebraic K L := by - apply @Algebra.isAlgebraic_of_subring_isAlgebraic (B ⧸ Q) - intro b_bar - have ⟨b, hb⟩ := Ideal.Quotient.mk_surjective b_bar - have hb : (algebraMap B (B ⧸ Q)) b = b_bar := hb - use ((M hFull b).map (algebraMap A (A ⧸ P))).map (algebraMap (A ⧸ P) K) - constructor - . apply ne_zero_of_ne_zero_of_monic X_ne_zero - apply Monic.map - apply Monic.map - exact M_monic hFull b - . rw [← hb, algebraMap_cast, map_map, ← IsScalarTower.algebraMap_eq] - rw [algebraMap_algebraMap, aeval_def, eval₂_eq_eval_map, map_map, ← IsScalarTower.algebraMap_eq] - rw [IsScalarTower.algebraMap_eq A B L, ← map_map, M_spec_map] - rw [eval_map, eval₂_hom, F_eval_eq_zero] - exact algebraMap.coe_zero - -include G in -theorem normal [DecidableEq L] : Normal K L := by - rw [normal_iff] - intro l - obtain ⟨f, hfmonic, _, hf, hfsplits⟩ := @f_exists G _ _ L _ K _ _ _ l - have hnz : f ≠ 0 := hfmonic.ne_zero - constructor - · rw [← isAlgebraic_iff_isIntegral] - exact ⟨f, hfmonic.ne_zero, hf⟩ - refine Polynomial.splits_of_splits_of_dvd (algebraMap K L) hnz hfsplits ?_ - exact minpoly.dvd _ _ hf - -open Module - -theorem separableClosure_finiteDimensional : FiniteDimensional K (separableClosure K L) := sorry - --- degree of max sep subextension is ≤ |G| -theorem separableClosure_finrank_le : finrank K (separableClosure K L) ≤ Nat.card G := sorry - -open scoped IntermediateField -theorem primitive_element : ∃ y : L, K⟮y⟯ = separableClosure K L := sorry - --- this definition might break when primitive_element is proved because there will be --- more hypotheses. -noncomputable def y : L := (primitive_element L K).choose - ---noncomputable def y_spec : K⟮y⟯ = separableClosure K L := (primitive_element L K).choose_spec - -end Bourbaki52222 - -end L_over_K_stuff - -section main_theorem_statement - -namespace Bourbaki52222 - -open scoped Pointwise - --- Basic API for what we're doing here. Writing down a map from the stabiliser of Q to --- the residual Galois group `L ≃ₐ[K] L`, where L=Frac(B/Q) and K=Frac(A/P). --- Hopefully sorrys aren't too hard - -def quotientRingAction (Q' : Ideal B) (g : G) (hg : g • Q = Q') : - B ⧸ Q ≃+* B ⧸ Q' := - Ideal.quotientEquiv Q Q' (MulSemiringAction.toRingEquiv G B g) hg.symm - -def quotientAlgebraAction (g : G) (hg : g • Q = Q) : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q where - __ := quotientRingAction Q Q g hg - commutes' := by - intro a_bar; dsimp - have ⟨a, ha⟩ := Ideal.Quotient.mk_surjective a_bar - rw [quotientRingAction]; dsimp - rw [← ha, ← Ideal.Quotient.algebraMap_eq, algebraMap_algebraMap] - rw [@Ideal.quotientMap_algebraMap A B _ _ _ B _ Q Q _ ] - simp - -def Pointwise.quotientAlgebraActionMonoidHom : - MulAction.stabilizer G Q →* ((B ⧸ Q) ≃ₐ[A ⧸ P] (B ⧸ Q)) where - toFun gh := quotientAlgebraAction Q P gh.1 gh.2 - map_one' := by - apply AlgEquiv.ext - intro b_bar; dsimp - unfold quotientAlgebraAction - unfold quotientRingAction - have ⟨b, hb⟩ := Ideal.Quotient.mk_surjective b_bar - rw [← hb, ← Ideal.Quotient.algebraMap_eq] - simp - map_mul' := by - intro ⟨x, hx⟩ ⟨y, hy⟩ - apply AlgEquiv.ext - intro b_bar; dsimp - unfold quotientAlgebraAction - unfold quotientRingAction - have ⟨b, hb⟩ := Ideal.Quotient.mk_surjective b_bar - rw [← hb, ← Ideal.Quotient.algebraMap_eq] - simp - rw [smul_smul] - -variable (L : Type*) [Field L] [Algebra (B ⧸ Q) L] [IsFractionRing (B ⧸ Q) L] - [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] - (K : Type*) [Field K] [Algebra (A ⧸ P) K] [IsFractionRing (A ⧸ P) K] - [Algebra K L] [IsScalarTower (A ⧸ P) K L] - - - -noncomputable def IsFractionRing.algEquiv_lift (e : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) : L ≃ₐ[K] L where - __ := IsFractionRing.ringEquivOfRingEquiv e.toRingEquiv - commutes' := by - intro k - dsimp - obtain ⟨x, y, _, rfl⟩ := @IsFractionRing.div_surjective (A ⧸ P) _ K _ _ _ k - simp [algebraMap_algebraMap] - unfold IsFractionRing.ringEquivOfRingEquiv - unfold IsLocalization.ringEquivOfRingEquiv - simp [IsScalarTower.algebraMap_apply (A ⧸ P) (B ⧸ Q) L] - -noncomputable def stabilizer.toGaloisGroup : MulAction.stabilizer G Q →* (L ≃ₐ[K] L) where - toFun gh := IsFractionRing.algEquiv_lift Q P L K (Pointwise.quotientAlgebraActionMonoidHom Q P gh) - map_one' := by - apply AlgEquiv.ext - intro l; simp - obtain ⟨x, y, _, rfl⟩ := @IsFractionRing.div_surjective (B ⧸ Q) _ L _ _ _ l - unfold IsFractionRing.algEquiv_lift - unfold IsFractionRing.ringEquivOfRingEquiv - simp - map_mul' := by - intro ⟨x, hx⟩ ⟨y, hy⟩ - apply AlgEquiv.ext - intro l; dsimp - obtain ⟨r, s, _, rfl⟩ := @IsFractionRing.div_surjective (B ⧸ Q) _ L _ _ _ l - unfold IsFractionRing.algEquiv_lift - unfold IsFractionRing.ringEquivOfRingEquiv - simp - sorry - -variable (hFull : ∀ (b : B), (∀ (g : G), g • b = b) ↔ ∃ a : A, b = a) in -/-- From Bourbaki Comm Alg, Chapter V. -/ -theorem MulAction.stabilizer_surjective_of_action : Function.Surjective - (stabilizer.toGaloisGroup Q P L K : MulAction.stabilizer G Q → (L ≃ₐ[K] L)) := by - sorry - -end Bourbaki52222 - -end main_theorem_statement - -section localization - -abbrev S := P.primeCompl -abbrev SA := A[(S P)⁻¹] - -abbrev SB := B[(S P)⁻¹] - --- Currently stuck here ---instance : Algebra (A[(S P)⁻¹]) (B[(S P)⁻¹]) where --- sorry--__ := OreLocalization.instModule (R := A) (X := B) (S := P.primeCompl) - -/- -failed to synthesize - Semiring (OreLocalization (S P) B) --/ -end localization - --- In Frobenius2.lean in this dir (Jou's FM24 project) there's a proof of surjectivity --- assuming B/Q is finite and P is maximal. --- Bourbaki reduce to maximal case by localizing at P, and use finite + separable = simple --- on the max separable subextension, but then the argument in Bourbaki closely --- follows Jou's formalisation in Frobenius2.lean in this directory, so this work will --- be useful later. -end part_b diff --git a/blueprint/src/chapter/FrobeniusProject.tex b/blueprint/src/chapter/FrobeniusProject.tex index 1716367b..71dac97c 100644 --- a/blueprint/src/chapter/FrobeniusProject.tex +++ b/blueprint/src/chapter/FrobeniusProject.tex @@ -471,7 +471,7 @@ \section{Proof of surjectivity.} by Jou Glasheen in the special case of number fields, in her final project for my Formalising Mathematics 2024 course. -A summary of the argument: we consider the monic degree $|G|$ polynomial $f_x$ in $K[X]$ or +The argument goes like this: we consider the monic degree $|G|$ polynomial $f_x$ in $K[X]$ or $\overline{M}_x$ in $(A/P)[X]$, which has $x$ and its G-conjugates as roots. If $\sigma\in\Aut_K(L)$ then $\sigma(\overline{x})$ is a root of $f$ as $\sigma$ fixes $K$ pointwise. Hence $\sigma(\overline{x})=\overline{g(x)}$ @@ -482,5 +482,5 @@ \section{Proof of surjectivity.} $L/M$ is purely inseparable. This argument is formalised and at the time of writing -is being \href{https://github.com/leanprover-community/mathlib4/pull/17717}{PRed to mathlib} +is being \href{https://github.com/leanprover-community/mathlib4/pull/19926}{PRed to mathlib} by Thomas Browning.