From 59700a13b0f5b8953655152b2c6c54d5e318698d Mon Sep 17 00:00:00 2001 From: Hu Yongle <2065545849@qq.com> Date: Sat, 26 Oct 2024 16:23:26 +0800 Subject: [PATCH] init --- .github/workflows/build.yaml | 23 + .gitignore | 1 + GaloisRamification.lean | 8 + GaloisRamification/GaloisRamification.lean | 467 ++++++++ .../Hilbert's_Ramification_Theory.lean | 1008 +++++++++++++++++ GaloisRamification/ToMathlib.lean | 133 +++ GaloisRamification/ToMathlib/Finite.lean | 60 + .../ToMathlib/FractionRing.lean | 13 + GaloisRamification/ToMathlib/Normal.lean | 17 + .../ToMathlib/restrictScalarsHom.lean | 29 + .../ToMathlib/separableClosure.lean | 33 + README.md | 1 + lake-manifest.json | 125 ++ lakefile.lean | 20 + lean-toolchain | 1 + 15 files changed, 1939 insertions(+) create mode 100644 .github/workflows/build.yaml create mode 100644 .gitignore create mode 100644 GaloisRamification.lean create mode 100644 GaloisRamification/GaloisRamification.lean create mode 100644 GaloisRamification/Hilbert's_Ramification_Theory.lean create mode 100644 GaloisRamification/ToMathlib.lean create mode 100644 GaloisRamification/ToMathlib/Finite.lean create mode 100644 GaloisRamification/ToMathlib/FractionRing.lean create mode 100644 GaloisRamification/ToMathlib/Normal.lean create mode 100644 GaloisRamification/ToMathlib/restrictScalarsHom.lean create mode 100644 GaloisRamification/ToMathlib/separableClosure.lean create mode 100644 README.md create mode 100644 lake-manifest.json create mode 100644 lakefile.lean create mode 100644 lean-toolchain diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml new file mode 100644 index 0000000..39496ce --- /dev/null +++ b/.github/workflows/build.yaml @@ -0,0 +1,23 @@ +name: Build +permissions: + contents: write +on: + push: + branches: + - "*" + pull_request: + branches: + - "*" +jobs: + build: + runs-on: ubuntu-latest + steps: + - name: Checkout Project + uses: actions/checkout@v4 + with: + fetch-depth: 2 + - name: Install Lean + run: | + curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s - -y --default-toolchain `cat ./lean-toolchain` + echo "$HOME/.elan/bin" >> $GITHUB_PATH + - run: lake exe cache get && lake build diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..bfb30ec --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/GaloisRamification.lean b/GaloisRamification.lean new file mode 100644 index 0000000..a9c9598 --- /dev/null +++ b/GaloisRamification.lean @@ -0,0 +1,8 @@ +import GaloisRamification.GaloisRamification +import GaloisRamification.Hilbert's_Ramification_Theory +import GaloisRamification.ToMathlib +import GaloisRamification.ToMathlib.Finite +import GaloisRamification.ToMathlib.FractionRing +import GaloisRamification.ToMathlib.Normal +import GaloisRamification.ToMathlib.restrictScalarsHom +import GaloisRamification.ToMathlib.separableClosure diff --git a/GaloisRamification/GaloisRamification.lean b/GaloisRamification/GaloisRamification.lean new file mode 100644 index 0000000..ab06f33 --- /dev/null +++ b/GaloisRamification/GaloisRamification.lean @@ -0,0 +1,467 @@ +/- +Copyright (c) 2024 Yongle Hu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yongle Hu +-/ +import Mathlib.Tactic +import Mathlib.NumberTheory.NumberField.Norm +import Mathlib.NumberTheory.RamificationInertia +import Mathlib.RingTheory.IntegralClosure.IntegralRestrict + +import GaloisRamification.ToMathlib + +set_option autoImplicit false + +/-! + +# Ramification theory in Galois extensions of number fields + +In this file, we discuss the ramification theory in Galois extensions of number fields, which is + also called Hilbert's Ramification Theory. + +## Main definitions and results + +* `isMaximal_conjugates` : The Galois group `Gal(K/L)` acts transitively on the set of all maximal ideals. +* `ramificationIdx_eq_of_isGalois` : In the case of Galois extension, +all the `ramificationIdx` are the same. +* `inertiaDeg_eq_of_isGalois`: In the case of Galois extension, all the `inertiaDeg` are the same. +* `DecompositionGroup` is consisting of all elements of the Galois group `L ≃ₐ[K] L` such +that keep `P` invariant. +* `inertiaDeg_of_DecompositionIdeal_over_bot_eq_oneThe` : The residue class field corresponding to +`DecompositionField p P` is isomorphic toresidue class field corresponding to `p`. +* `InertiaGroup` is the subgorup of `L ≃ₐ[K] L` that consists of all +the `σ : L ≃ₐ[K] L` that are identity modulo `P`. + +## References + + * [J Neukirch, *Algebraic Number Theory*][Neukirch1992] + +-/ + + +open Algebra Ideal + +open scoped BigOperators + +attribute [local instance] FractionRing.liftAlgebra Quotient.field FractionRing.isScalarTower_liftAlgebra + +/-! ### lies over -/ + +section lie_over + +namespace Ideal + +variable {A : Type*} [CommRing A] (p : Ideal A) [p.IsMaximal] (B : Type*) [CommRing B] [Nontrivial B] + [Algebra A B] [NoZeroSMulDivisors A B] [Algebra.IsIntegral A B] + +/-- For any maximal idela `p` in `A`, there exists a maximal ideal in `B` lying over `p`. -/ +noncomputable def over_isMaximal : Ideal B := + Classical.choose <| exists_ideal_over_maximal_of_isIntegral p <| + (NoZeroSMulDivisors.ker_algebraMap_eq_bot A B).trans_le bot_le + +instance isMaximal_of_over_isMaximal : (p.over_isMaximal B).IsMaximal := + (Classical.choose_spec <| exists_ideal_over_maximal_of_isIntegral p <| + (NoZeroSMulDivisors.ker_algebraMap_eq_bot A B).trans_le bot_le).1 + +instance lies_over_of_over_isMaximal : (p.over_isMaximal B).LiesOver p where + over := (Classical.choose_spec <| exists_ideal_over_maximal_of_isIntegral p <| + (NoZeroSMulDivisors.ker_algebraMap_eq_bot A B).trans_le bot_le).2.symm + +attribute [irreducible] over_isMaximal + +end Ideal + + + +variable {A B : Type*} [CommRing A] [IsDedekindDomain A] [CommRing B] [IsDedekindDomain B] + [Algebra A B] [Algebra.IsIntegral A B] (p : Ideal A) (P : Ideal B) [ho : P.LiesOver p] + +open scoped Classical in +/-- The `Finset` consists of all primes lying over `p : Ideal A`. -/ +noncomputable abbrev primes_over (B : Type*) [CommRing B] [IsDedekindDomain B] [Algebra A B] : + Finset (Ideal B) := + (UniqueFactorizationMonoid.factors (map (algebraMap A B) p)).toFinset + +/- /-- The image of a maximal ideal under the algebraMap between ring of integers is non-zero. -/ +theorem Ideal.map_isMaximal_ne_bot (hp0 : p ≠ ⊥) : map (algebraMap A B) p ≠ ⊥ := sorry -/ + +theorem prime_iff_isMaximal {p : Ideal A} (hp0 : p ≠ ⊥) : Prime p ↔ p.IsMaximal := + ⟨fun hp ↦ (isPrime_of_prime hp).isMaximal hp.ne_zero, + fun hp ↦ prime_of_isPrime hp0 hp.isPrime⟩ + +namespace Ideal +-- lemmas of isomorphisms act on ideals +/-- A ring isomorphism sends a prime ideal to a prime ideal. -/ +instance {R S E : Type*} [CommRing R] [CommRing S] (p : Ideal R) [p.IsPrime] [EquivLike E R S] + [RingEquivClass E R S] (e : E) : (map e p).IsPrime := by + exact map_isPrime_of_equiv e + +/-- A ring isomorphism sends a maximal ideal to a maximal ideal. -/ +instance map_isMaximal_of_equiv {R S E : Type*} [Ring R] [Ring S] (p : Ideal R) + [hp : p.IsMaximal] [EquivLike E R S] [RingEquivClass E R S] (e : E) : (map e p).IsMaximal := + map.isMaximal e (EquivLike.bijective e) hp + +/-- A maximal ideal pull back by a ring isomorphism is a maximal ideal. -/ +instance comap_isMaximal_of_equiv {R S E : Type*} [Ring R] [Ring S] (p : Ideal S) + [p.IsMaximal] [EquivLike E R S] [RingEquivClass E R S] (e : E) : (comap e p).IsMaximal := + comap_isMaximal_of_surjective e (EquivLike.surjective e) + +theorem mem_map_of_equiv {R S E : Type*} [Semiring R] [Semiring S] (I : Ideal R) + [EquivLike E R S] [RingEquivClass E R S] (e : E) (y : S) : y ∈ map e I ↔ ∃ x ∈ I, e x = y := by + constructor + · intro h + simp_rw [show map e I = _ from map_comap_of_equiv I (e : R ≃+* S)] at h + exact ⟨(e : R ≃+* S).symm y, h, RingEquiv.apply_symm_apply (e : R ≃+* S) y⟩ + · rintro ⟨x, hx, rfl⟩ + exact mem_map_of_mem e hx + +#check Ideal.map_comap_of_equiv + +end Ideal + +end lie_over + +section + +/-! ### Galois group `Gal(K/L)` acts transitively on the set of all maximal ideals -/ + +variable {A B : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [CommRing B] [IsDomain B] + [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] [NoZeroSMulDivisors A B] + [IsGalois (FractionRing A) (FractionRing B)] + (p : Ideal A) (P : Ideal B) [P.IsMaximal] [P.LiesOver p] + +theorem isMaximal_conjugates_of_isGalois (Q : Ideal B) [hqm : Q.IsMaximal] [Q.LiesOver p] : + ∃ σ : B ≃ₐ[A] B, map σ P = Q := by + by_contra hs + push_neg at hs + rcases Submodule.mem_sup.mp <| (eq_top_iff_one (Q ⊔ ∏ σ : B ≃ₐ[A] B, map σ P)).mp <| + sup_prod_eq_top fun σ _ ↦ hqm.coprime_of_ne inferInstance (hs σ).symm + with ⟨x, hx, y, hy, hxy⟩ + let n : B := ∏ σ : B ≃ₐ[A] B, σ x + have hnx : n = (algebraMap A B) (intNorm A B x) := (algebraMap_intNorm_of_isGalois A B).symm + have hnk : intNorm A B x ∈ P.under A := by + rw [← P.over_def p, Q.over_def p, mem_comap, ← hnx] + refine (span_singleton_le_iff_mem Q).mp ?_ + rw [← prod_span_singleton] + exact hqm.isPrime.prod_le.mpr ⟨1, Finset.mem_univ 1, (span_singleton_le_iff_mem Q).mpr hx⟩ + rcases IsPrime.prod_mem_iff.mp (Eq.mpr (hnx ▸ Eq.refl (n ∈ P)) hnk : n ∈ P) with ⟨σ, _, hs⟩ + have hxp : x ∈ map σ.symm P := by + rw [← AlgEquiv.symm_apply_apply σ x] + exact mem_map_of_mem σ.symm hs + have h := Ideal.add_mem (map σ.symm P) hxp <| + (prod_le_inf.trans (Finset.inf_le (Finset.mem_univ σ.symm))) hy + rw [hxy] at h + exact IsMaximal.ne_top inferInstance ((eq_top_iff_one _).mpr h) + +end + +section + +namespace Ideal + +variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] + +/-- The algebra equiv `(B ⧸ P) ≃ₐ[A ⧸ p] (B ⧸ map (mapRingHom σ) P)` + induced by an algebra equiv `σ : L ≃ₐ[K] L`. -/ +def quotientAlgEquiv {p : Ideal A} {P : Ideal B} [P.LiesOver p] + {Q : Ideal B} [Q.LiesOver p] (σ : B ≃ₐ[A] B) (hs : map σ P = Q) : + (B ⧸ P) ≃ₐ[A ⧸ p] (B ⧸ Q) := { + quotientEquiv P Q σ (by rw [← hs]; rfl) with + commutes' := by + rintro ⟨x⟩ + exact congrArg (Ideal.Quotient.mk Q) (AlgEquiv.commutes σ x) +} + +/-- `MonoidHom` version of `Ideal.quotientAlgEquiv`. -/ +def quotientAlgEquivHom (p : Ideal A) (P : Ideal B) [P.LiesOver p] + (h : ∀ σ : B ≃ₐ[A] B, map σ P = P) : (B ≃ₐ[A] B) →* ((B ⧸ P) ≃ₐ[A ⧸ p] (B ⧸ P)) where + toFun σ := quotientAlgEquiv σ (h σ) + map_one' := by ext ⟨⟩; rfl + map_mul' _ _ := by ext ⟨⟩; rfl + +open Polynomial IntermediateField + +section + +variable [IsDomain A] [IsIntegrallyClosed A] [IsDomain B] [IsIntegrallyClosed B] + [Module.Finite A B] [NoZeroSMulDivisors A B] [hn : Normal (FractionRing A) (FractionRing B)] + (p : Ideal A) (P : Ideal B) [p.IsMaximal] [P.IsMaximal] [P.LiesOver p] + (h : ∀ σ : B ≃ₐ[A] B, map σ P = P) [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] + +theorem quotientAlgEquivHom_surjective'' : + Function.Surjective (quotientAlgEquivHom p P h) := by + let K := FractionRing A + let L := FractionRing B + let F := A ⧸ p + let E := B ⧸ P + have e : PowerBasis F E := Field.powerBasisOfFiniteOfSeparable F E + intro σ + let β := (PowerBasis.liftEquiv e).toFun σ.toAlgHom + rcases Quotient.exists_rep e.gen with ⟨a, ha⟩ + let f : A[X] := minpoly A a + let fl : B[X] := f.map (algebraMap A B) + let ϕp : A →+* F := Ideal.Quotient.mk p + let ϕP : B →+* E := Ideal.Quotient.mk P + have hq : ⟦a⟧ = ϕP a := rfl + rw [hq] at ha + have hai : IsIntegral A a := IsIntegral.isIntegral a + have hm : f.Monic := minpoly.monic hai + have h0 : (fl.map ϕP) ≠ 0 := map_monic_ne_zero (Monic.map (algebraMap A B) hm) + have hbr : β.1 ∈ (fl.map ϕP).roots := by + have h : aeval e.gen (f.map ϕp) = ϕP (aeval a f) := by + rw [← ha] + exact (@map_aeval_eq_aeval_map _ _ _ F E _ _ _ _ _ ϕp ϕP rfl f a).symm + rw [minpoly.aeval, map_zero] at h + apply (mem_roots_iff_aeval_eq_zero h0).mpr + have hc : fl.map ϕP = (f.map ϕp).map (algebraMap F E) := by + rw [Polynomial.map_map, Polynomial.map_map] + rfl + have hbz := aeval_eq_zero_of_dvd_aeval_eq_zero (minpoly.dvd F e.gen h) β.2 + simp only [Equiv.toFun_as_coe, AlgEquiv.toAlgHom_eq_coe, PowerBasis.liftEquiv_apply_coe, + AlgHom.coe_coe, hc, aeval_map_algebraMap, ← hbz] + have hfe : (Polynomial.map (algebraMap A K) f) = minpoly K (algebraMap B L a) := by + refine minpoly.eq_of_irreducible_of_monic + ((Monic.irreducible_iff_irreducible_map_fraction_map (minpoly.monic hai)).mp + (minpoly.irreducible hai)) ?_ (Monic.map (algebraMap A K) (minpoly.monic hai)) + simp only [aeval_map_algebraMap, aeval_algebraMap_eq_zero_iff, minpoly.aeval, f] + have h : fl.roots.map ϕP = (fl.map ϕP).roots := by + have h := (natDegree_eq_card_roots' (hn.splits (algebraMap B L a))).symm + rw [← hfe, natDegree_map, Monic.natDegree_map (minpoly.monic hai), Polynomial.map_map, + ← IsScalarTower.algebraMap_eq A K L, + ← isIntegralClosure_root_card_eq_ofMonic B L (minpoly.monic hai), + ← Monic.natDegree_map (minpoly.monic hai) (algebraMap A B)] at h + exact roots_map_of_card_eq_natDegree h0 h + rw [← h] at hbr + rcases Multiset.mem_map.mp hbr with ⟨b, ⟨hbr, hb⟩⟩ + have h : aeval (algebraMap B L b) (minpoly K (AdjoinSimple.gen K (algebraMap B L a))) = 0 := by + have he : minpoly K (AdjoinSimple.gen K (algebraMap B L a)) = minpoly K (algebraMap B L a) := + minpoly_eq (AdjoinSimple.gen K ((algebraMap B L) a)) + rw [he, ← hfe, aeval_map_algebraMap, aeval_algebraMap_eq_zero_iff, aeval_def, ← eval_map, + ← coe_aeval_eq_eval, (mem_roots_iff_aeval_eq_zero (map_monic_ne_zero hm)).mp hbr] + let ε := IntermediateField.adjoin.powerBasis (hn.isIntegral (algebraMap B L a)) + let τ : L ≃ₐ[K] L := (ε.lift (algebraMap B L b) h).fieldRangeAlgEquiv.liftNormal L + use galRestrict A K L B τ + refine AlgEquiv.coe_algHom_injective (e.liftEquiv.injective ?_) + apply Subtype.val_inj.mp + rw [e.liftEquiv_apply_coe, AlgHom.coe_coe] + simp only [← ha, Equiv.toFun_as_coe, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_coe] + show ϕP ((galRestrict A K L B τ) a) = β.1 + rw [← hb] + exact congrArg ϕP <| NoZeroSMulDivisors.algebraMap_injective B L <| + (algebraMap_galRestrict_apply A τ a).trans <| + ((ε.lift (algebraMap B L b) h).fieldRangeAlgEquiv.liftNormal_commutes L + (AdjoinSimple.gen K (algebraMap B L a))).trans (ε.lift_gen (algebraMap B L b) h) + +end + +section + +variable {A B : Type*} [CommRing A] [IsIntegrallyClosed A] [CommRing B] [IsDomain B] [Algebra A B] + [Module.Finite A B] (p : Ideal A) (P : Ideal B) [p.IsMaximal] [P.IsMaximal] [P.LiesOver p] + (h : ∀ σ : B ≃ₐ[A] B, map σ P = P) + (K L : Type*) [Field K] [Field L] [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] [hn : Normal K L] + +include K L +theorem quotientAlgEquivHom_surjective' : + Function.Surjective (quotientAlgEquivHom p P h) := sorry/- by + haveI := (IsFractionRing.injective A K).isDomain + haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B + let F := A ⧸ p + let E := B ⧸ P + have e : PowerBasis F (separableClosure F E) := Field.powerBasisOfFiniteOfSeparable F _ + intro σ + have := σ.restrictNormal (separableClosure F E) + let β := (PowerBasis.liftEquiv e).toFun σ.restrictNormal.toAlgHom + rcases Quotient.exists_rep e.gen with ⟨a, ha⟩ + let f : A[X] := minpoly A a + let fl : B[X] := f.map (algebraMap A B) + let ϕp : A →+* F := Ideal.Quotient.mk p + let ϕP : B →+* E := Ideal.Quotient.mk P + have hq : ⟦a⟧ = ϕP a := rfl + rw [hq] at ha + have hai : IsIntegral A a := IsIntegral.isIntegral a + have hm : f.Monic := minpoly.monic hai + have h0 : (fl.map ϕP) ≠ 0 := map_monic_ne_zero (Monic.map (algebraMap A B) hm) + have hbr : β.1 ∈ (fl.map ϕP).roots := by + have h : aeval e.gen (f.map ϕp) = ϕP (aeval a f) := by + rw [← ha] + exact (@map_aeval_eq_aeval_map _ _ _ F E _ _ _ _ _ ϕp ϕP rfl f a).symm + rw [minpoly.aeval, map_zero] at h + apply (mem_roots_iff_aeval_eq_zero h0).mpr + have hc : fl.map ϕP = (f.map ϕp).map (algebraMap F E) := by + rw [Polynomial.map_map, Polynomial.map_map] + rfl + have hbz := aeval_eq_zero_of_dvd_aeval_eq_zero (minpoly.dvd F e.gen h) β.2 + simp only [Equiv.toFun_as_coe, AlgEquiv.toAlgHom_eq_coe, PowerBasis.liftEquiv_apply_coe, + AlgHom.coe_coe, hc, aeval_map_algebraMap, ← hbz] + have hfe : (Polynomial.map (algebraMap A K) f) = minpoly K (algebraMap B L a) := by + refine minpoly.eq_of_irreducible_of_monic + ((Monic.irreducible_iff_irreducible_map_fraction_map (minpoly.monic hai)).mp + (minpoly.irreducible hai)) ?_ (Monic.map (algebraMap A K) (minpoly.monic hai)) + simp only [aeval_map_algebraMap, aeval_algebraMap_eq_zero_iff, minpoly.aeval, f] + have h : fl.roots.map ϕP = (fl.map ϕP).roots := by + have h := (natDegree_eq_card_roots' (hn.splits (algebraMap B L a))).symm + rw [← hfe, natDegree_map, Monic.natDegree_map (minpoly.monic hai), Polynomial.map_map, + ← IsScalarTower.algebraMap_eq A K L, + ← isIntegralClosure_root_card_eq_ofMonic B L (minpoly.monic hai), + ← Monic.natDegree_map (minpoly.monic hai) (algebraMap A B)] at h + exact roots_map_of_card_eq_natDegree h0 h + rw [← h] at hbr + rcases Multiset.mem_map.mp hbr with ⟨b, ⟨hbr, hb⟩⟩ + have h : aeval (algebraMap B L b) (minpoly K (AdjoinSimple.gen K (algebraMap B L a))) = 0 := by + have he : minpoly K (AdjoinSimple.gen K (algebraMap B L a)) = minpoly K (algebraMap B L a) := + minpoly_eq (AdjoinSimple.gen K ((algebraMap B L) a)) + rw [he, ← hfe, aeval_map_algebraMap, aeval_algebraMap_eq_zero_iff, aeval_def, ← eval_map, + ← coe_aeval_eq_eval, (mem_roots_iff_aeval_eq_zero (map_monic_ne_zero hm)).mp hbr] + let ε := IntermediateField.adjoin.powerBasis (hn.isIntegral (algebraMap B L a)) + let τ : L ≃ₐ[K] L := (ε.lift (algebraMap B L b) h).fieldRangeAlgEquiv.liftNormal L + use galRestrict A K L B τ + refine AlgEquiv.coe_algHom_injective (e.liftEquiv.injective ?_) + apply Subtype.val_inj.mp + rw [e.liftEquiv_apply_coe, AlgHom.coe_coe] + simp only [← ha, Equiv.toFun_as_coe, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_coe] + show ϕP ((galRestrict A K L B τ) a) = β.1 + rw [← hb] + exact congrArg ϕP <| NoZeroSMulDivisors.algebraMap_injective B L <| + (algebraMap_galRestrict_apply A τ a).trans <| + ((ε.lift (algebraMap B L b) h).fieldRangeAlgEquiv.liftNormal_commutes L + (AdjoinSimple.gen K (algebraMap B L a))).trans (ε.lift_gen (algebraMap B L b) h) -/ + +end + +section + +variable {A B : Type*} [CommRing A] [IsIntegrallyClosed A] [CommRing B] [IsDomain B] [Algebra A B] + [Module.Finite A B] (p : Ideal A) (P : Ideal B) [p.IsMaximal] [P.IsMaximal] [P.LiesOver p] + (h : ∀ σ : B ≃ₐ[A] B, map σ P = P) [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] + (K L : Type*) [Field K] [Field L] [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] [hn : Normal K L] + +include K L +theorem quotientAlgEquivHom_surjective : + Function.Surjective (quotientAlgEquivHom p P h) := by + haveI := (IsFractionRing.injective A K).isDomain + haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B + let F := A ⧸ p + let E := B ⧸ P + have e : PowerBasis F E := Field.powerBasisOfFiniteOfSeparable F E + intro σ + let β := (PowerBasis.liftEquiv e).toFun σ.toAlgHom + rcases Quotient.exists_rep e.gen with ⟨a, ha⟩ + let f : A[X] := minpoly A a + let fl : B[X] := f.map (algebraMap A B) + let ϕp : A →+* F := Ideal.Quotient.mk p + let ϕP : B →+* E := Ideal.Quotient.mk P + have hq : ⟦a⟧ = ϕP a := rfl + rw [hq] at ha + have hai : IsIntegral A a := IsIntegral.isIntegral a + have hm : f.Monic := minpoly.monic hai + have h0 : (fl.map ϕP) ≠ 0 := map_monic_ne_zero (Monic.map (algebraMap A B) hm) + have hbr : β.1 ∈ (fl.map ϕP).roots := by + have h : aeval e.gen (f.map ϕp) = ϕP (aeval a f) := by + rw [← ha] + exact (@map_aeval_eq_aeval_map _ _ _ F E _ _ _ _ _ ϕp ϕP rfl f a).symm + rw [minpoly.aeval, map_zero] at h + apply (mem_roots_iff_aeval_eq_zero h0).mpr + have hc : fl.map ϕP = (f.map ϕp).map (algebraMap F E) := by + rw [Polynomial.map_map, Polynomial.map_map] + rfl + have hbz := aeval_eq_zero_of_dvd_aeval_eq_zero (minpoly.dvd F e.gen h) β.2 + simp only [Equiv.toFun_as_coe, AlgEquiv.toAlgHom_eq_coe, PowerBasis.liftEquiv_apply_coe, + AlgHom.coe_coe, hc, aeval_map_algebraMap, ← hbz] + have hfe : (Polynomial.map (algebraMap A K) f) = minpoly K (algebraMap B L a) := by + refine minpoly.eq_of_irreducible_of_monic + ((Monic.irreducible_iff_irreducible_map_fraction_map (minpoly.monic hai)).mp + (minpoly.irreducible hai)) ?_ (Monic.map (algebraMap A K) (minpoly.monic hai)) + simp only [aeval_map_algebraMap, aeval_algebraMap_eq_zero_iff, minpoly.aeval, f] + have h : fl.roots.map ϕP = (fl.map ϕP).roots := by + have h := (natDegree_eq_card_roots' (hn.splits (algebraMap B L a))).symm + rw [← hfe, natDegree_map, Monic.natDegree_map (minpoly.monic hai), Polynomial.map_map, + ← IsScalarTower.algebraMap_eq A K L, + ← isIntegralClosure_root_card_eq_ofMonic B L (minpoly.monic hai), + ← Monic.natDegree_map (minpoly.monic hai) (algebraMap A B)] at h + exact roots_map_of_card_eq_natDegree h0 h + rw [← h] at hbr + rcases Multiset.mem_map.mp hbr with ⟨b, ⟨hbr, hb⟩⟩ + have h : aeval (algebraMap B L b) (minpoly K (AdjoinSimple.gen K (algebraMap B L a))) = 0 := by + have he : minpoly K (AdjoinSimple.gen K (algebraMap B L a)) = minpoly K (algebraMap B L a) := + minpoly_eq (AdjoinSimple.gen K ((algebraMap B L) a)) + rw [he, ← hfe, aeval_map_algebraMap, aeval_algebraMap_eq_zero_iff, aeval_def, ← eval_map, + ← coe_aeval_eq_eval, (mem_roots_iff_aeval_eq_zero (map_monic_ne_zero hm)).mp hbr] + let ε := IntermediateField.adjoin.powerBasis (hn.isIntegral (algebraMap B L a)) + let τ : L ≃ₐ[K] L := (ε.lift (algebraMap B L b) h).fieldRangeAlgEquiv.liftNormal L + use galRestrict A K L B τ + refine AlgEquiv.coe_algHom_injective (e.liftEquiv.injective ?_) + apply Subtype.val_inj.mp + rw [e.liftEquiv_apply_coe, AlgHom.coe_coe] + simp only [← ha, Equiv.toFun_as_coe, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_coe] + show ϕP ((galRestrict A K L B τ) a) = β.1 + rw [← hb] + exact congrArg ϕP <| NoZeroSMulDivisors.algebraMap_injective B L <| + (algebraMap_galRestrict_apply A τ a).trans <| + ((ε.lift (algebraMap B L b) h).fieldRangeAlgEquiv.liftNormal_commutes L + (AdjoinSimple.gen K (algebraMap B L a))).trans (ε.lift_gen (algebraMap B L b) h) + +end + +end Ideal + +end + +-- 之后都用 isMaximal_conjugates 取出 σ : B ≃ₐ[A] B, 不必取 σ : L ≃ₐ[K] L + + +/- +variable {A B : Type*} [CommRing A] [CommRing B] [IsDedekindDomain B] + [Algebra A B] (K L : Type*) [Field K] [Field L] [IsDedekindDomain A] + [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] [Algebra K L] + [FiniteDimensional K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] + [IsIntegralClosure B A L] (p : Ideal A) (hp0 : p ≠ ⊥) (P : Ideal B) [hpm : P.IsMaximal] + [hp : P lies_over p] (Q : Ideal B) [hqm : Q.IsMaximal] [hq : Q lies_over p] [IsGalois K L] (σ : L ≃ₐ[K] L) + +include p hp0 in +/-- The Galois group `Gal(K/L)` acts transitively on the set of all maximal ideals `P` of `𝓞 L` +lying above `p`, i.e., these prime ideals are all conjugates of each other. -/ +theorem isMaximal_conjugates' : ∃ σ : L ≃ₐ[K] L, map (galRestrict A K L B σ) P = Q := by + by_contra hs + push_neg at hs + let s : Finset (L ≃ₐ[K] L) := Finset.univ + sorry/- have : ∃ y ∈ Q, ∃ z ∈ ∏ σ ∈ s, map (galRestrict A K L B σ) P, y + z = 1 := by + apply Submodule.mem_sup.mp + apply (eq_top_iff_one (Q ⊔ ∏ σ in s, map (galRestrict A K L B σ) P)).mp + apply sup_prod_eq_top + intro σ _ + apply IsMaximal.coprime_of_ne hqm + rcases Submodule.mem_sup.mp <| (eq_top_iff_one (Q ⊔ ∏ σ in s, map (galRestrict A K L B σ) P)).mp <| + sup_prod_eq_top <| fun σ _ ↦ IsMaximal.coprime_of_ne hqm (GalRingHom_map.isMaximal P σ) + (hs σ).symm with ⟨x, hx, y, hy, hxy⟩ + let n : 𝓞 L := ∏ σ in s, (galRestrict A K L B σ) x + have hnx : n = (algebraMap A B) (RingOfIntegers.norm K x) := + Subtype.val_inj.mp <| Eq.trans + (Submonoid.coe_finset_prod (integralClosure ℤ L).toSubmonoid (fun i ↦ (GalRingHom i) x) s) + (Algebra.norm_eq_prod_automorphisms K x.1).symm + have hnk : RingOfIntegers.norm K x ∈ idealUnder K P := by + rw [idealUnder, ← hp.over, hq.over] + apply mem_comap.mpr + rw [← hnx] + refine (span_singleton_le_iff_mem Q).mp ?_ + rw [← prod_span_singleton] + exact prod_le_inf.trans <| (@Finset.inf_le _ _ _ _ s (fun σ ↦ span {(galRestrict A K L B σ) x}) _ + (@Finset.mem_univ (L ≃ₐ[K] L) _ 1)).trans (Iff.mpr (span_singleton_le_iff_mem Q) hx) + have hnp : n ∈ P := Eq.mpr (_root_.id (hnx ▸ Eq.refl (n ∈ P))) hnk + rcases IsPrime.prod_mem hnp with ⟨⟨σ, _⟩, hs⟩ + have hxp : x ∈ map (GalRingHom σ⁻¹) P := Eq.mpr + ((GalRingHom_inv_mul_cancel_mem σ x).symm ▸ Eq.refl _) (mem_map_of_mem (GalRingHom σ⁻¹) hs) + have h := Ideal.add_mem (map (GalRingHom σ⁻¹) P) hxp <| + (prod_le_inf.trans (Finset.inf_le (Finset.mem_univ σ⁻¹))) hy + rw [hxy] at h + exact IsMaximal.ne_top (GalRingHom_map.isMaximal P σ⁻¹) ((eq_top_iff_one _).mpr h) -/ + +include K L p hp0 in +theorem isMaximal_conjugates : ∃ σ : B ≃ₐ[A] B, map σ P = Q := by + rcases isMaximal_conjugates' K L p hp0 P Q with ⟨σ, hs⟩ + exact ⟨galRestrict A K L B σ, hs⟩ + -/ diff --git a/GaloisRamification/Hilbert's_Ramification_Theory.lean b/GaloisRamification/Hilbert's_Ramification_Theory.lean new file mode 100644 index 0000000..7e58205 --- /dev/null +++ b/GaloisRamification/Hilbert's_Ramification_Theory.lean @@ -0,0 +1,1008 @@ +/- +Copyright (c) 2023 Hu Yongle. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Hu Yongle +-/ +import Mathlib.Tactic +import Mathlib.NumberTheory.NumberField.Norm +import Mathlib.NumberTheory.RamificationInertia + +import GaloisRamification.ToMathlib + +set_option autoImplicit false + +set_option synthInstance.maxHeartbeats 25000 + +/-! + +# Hilbert's Ramification Theory + +In this file, we discuss the ramification theory in Galois extensions of number fields. + +## Main definitions and results + +* `isMaximal_conjugates` : The Galois group `Gal(K/L)` acts transitively on the set of all maximal ideals. +* `ramificationIdx_eq_of_isGalois` : In the case of Galois extension, +all the `ramificationIdx` are the same. +* `inertiaDeg_eq_of_isGalois`: In the case of Galois extension, all the `inertiaDeg` are the same. +* `decompositionGroup` is consisting of all elements of the Galois group `L ≃ₐ[K] L` such +that keep `P` invariant. +* `inertiaDeg_of_decompositionideal_over_bot_eq_oneThe` : The residue class field corresponding to +`decompositionField p P` is isomorphic toresidue class field corresponding to `p`. +* `inertiaGroup` is the subgorup of `L ≃ₐ[K] L` that consists of all +the `σ : L ≃ₐ[K] L` that are identity modulo `P`. + +## References + + * [J Neukirch, *Algebraic Number Theory*][Neukirch1992] + +-/ + +open Algebra Ideal + +open scoped BigOperators + +attribute [local instance] Ideal.Quotient.field + +/-! ### Preliminary -/ + +namespace NumberField + +open RingOfIntegers + +section preparation + +variable (K : Type*) [Field K] {L : Type*} [Field L] [Algebra K L] + (P : Ideal (𝓞 L)) (p : Ideal (𝓞 K)) + +/-- The ideal obtained by intersecting `𝓞 K` and `P`. -/ +abbrev idealUnder : Ideal (𝓞 K) := comap (algebraMap (𝓞 K) (𝓞 L)) P + +theorem idealUnder_def : idealUnder K P = comap (algebraMap (𝓞 K) (𝓞 L)) P := rfl + +instance idealUnder.IsPrime [P.IsPrime] : IsPrime (idealUnder K P) := + IsPrime.comap (algebraMap (𝓞 K) (𝓞 L)) + +variable {K L : Type*} [Field K] [Field L] [Algebra K L] (P : Ideal (𝓞 L)) (p : Ideal (𝓞 K)) + +/-- We say `P` lies over `p` if `p` is the preimage of `P` under the `algebraMap`. -/ +-- We introduce this class to address the type class inference problem for `(B ⧸ P) ≃ₐ[A ⧸ p] (B ⧸ P) `. +class ideal_lies_over : Prop where over : p = comap (algebraMap (𝓞 K) (𝓞 L)) P + +@[inherit_doc] infix : 50 "lies_over" => ideal_lies_over + +instance over_idealUnder : P lies_over (idealUnder K P) where over := rfl + +class ideal_unique_lies_over extends ideal_lies_over P p : Prop where + unique : ∀ Q : Ideal (𝓞 L), [Q.IsMaximal] → [Q lies_over p] → Q = P + +infix : 50 "unique_lies_over" => ideal_unique_lies_over + +variable [NumberField L] (p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) [p.IsMaximal] [P.IsMaximal] +[P lies_over p] + +/-- If `P` is a maximal ideal of `𝓞 L`, then the intersection of `P` and `𝓞 K` is also +a maximal ideal. -/ +instance idealUnder.IsMaximal : IsMaximal (idealUnder K P) := + isMaximal_comap_of_isIntegral_of_isMaximal P + +/-- In particular, if `p` is a maximal ideal of `ringOfIntegers`, then +the intersection of `p` and `ℤ` is also a maximal ideal. -/ +instance ideal_comap_int.IsMaximal [NumberField K] (p : Ideal (𝓞 K)) [p.IsMaximal] : + IsMaximal (comap (algebraMap ℤ (𝓞 K)) p) := isMaximal_comap_of_isIntegral_of_isMaximal p + +/-- For any maximal idela `p` in `𝓞 K`, there exists a maximal ideal in `𝓞 L` lying over `p`. -/ +theorem exists_ideal_over_maximal_of_ringOfIntegers (p : Ideal (𝓞 K)) [p.IsMaximal] + (L : Type*) [Field L] [NumberField L] [Algebra K L] : + ∃ (P : Ideal (𝓞 L)), IsMaximal P ∧ P lies_over p := by + rcases exists_ideal_over_maximal_of_isIntegral (S := 𝓞 L) p + (by simp only [ker_algebraMap_eq_bot K L, bot_le]) with ⟨P, hpm, hp⟩ + exact ⟨P, hpm, ideal_lies_over.mk hp.symm⟩ + +/-- Maximal Ideals in the ring of integers are non-zero. -/ +theorem ne_bot_ofIsMaximal [NumberField K] : p ≠ ⊥ := + Ring.ne_bot_of_isMaximal_of_not_isField inferInstance (RingOfIntegers.not_isField K) + +/-- The image of a maximal ideal under the algebraMap between ring of integers is non-zero. -/ +theorem map_isMaximal_ne_bot [NumberField K] (p : Ideal (𝓞 K)) [p.IsMaximal] + (L : Type*) [Field L] [Algebra K L] : map (algebraMap (𝓞 K) (𝓞 L)) p ≠ ⊥ := + fun h ↦ (ne_bot_ofIsMaximal p) ((map_eq_bot_iff_of_injective (algebraMap.injective K L)).mp h) + +theorem prime_iff_isMaximal (P : Ideal (𝓞 L)) : Prime P ↔ IsMaximal P := + ⟨fun hp ↦ IsPrime.isMaximal (isPrime_of_prime hp) (Prime.ne_zero hp), + fun hp ↦ prime_of_isPrime (ne_bot_ofIsMaximal P) (IsMaximal.isPrime hp)⟩ + +open Classical in +/-- The `Finset` consists of all primes lying over `p : Ideal (𝓞 K)`. -/ +noncomputable abbrev primes_over {K : Type*} [Field K] (p : Ideal (𝓞 K)) + (L : Type*) [Field L] [NumberField L] [Algebra K L] : Finset (Ideal (𝓞 L)) := + (UniqueFactorizationMonoid.factors (map (algebraMap (𝓞 K) (𝓞 L)) p)).toFinset + +open UniqueFactorizationMonoid + +variable {K L : Type*} [Field K] [NumberField K] [Field L] [NumberField L] +[Algebra K L] (p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) [p.IsMaximal] + +theorem primes_over_mem : + P ∈ primes_over p L ↔ P.IsMaximal ∧ P lies_over p := by + constructor + · intro hp + classical have hp := Multiset.mem_toFinset.mp hp + have hpm := (prime_iff_isMaximal P).mp (prime_of_factor P hp) + exact ⟨hpm, ideal_lies_over.mk <| IsMaximal.eq_of_le inferInstance (comap_ne_top _ (IsMaximal.ne_top hpm)) + (le_comap_of_map_le (le_of_dvd (dvd_of_mem_factors hp)))⟩ + · intro ⟨hpm, hp⟩ + have hd := dvd_iff_le.mpr (map_le_of_le_comap (le_of_eq hp.over)) + have hir := irreducible_iff_prime.mpr ((prime_iff_isMaximal P).mpr hpm) + rcases exists_mem_factors_of_dvd (map_isMaximal_ne_bot p L) hir hd with ⟨_, hq, he⟩ + classical rw [Multiset.mem_toFinset, associated_iff_eq.mp he] + exact hq + +instance primes_over_instIsMaximal (Q : primes_over p L) : IsMaximal Q.1 := + ((primes_over_mem p Q.1).mp Q.2).1 + +instance primes_over_inst_lies_over (Q : primes_over p L) : Q.1 lies_over p := + ((primes_over_mem p Q.1).mp Q.2).2 + +/-- Given a maximal ideal `P lies_over p` in `𝓞 L`, `primes_over.mk` sends `P` to an element of +the subset `primes_over p L` of `Ideal (𝓞 L)`. -/ +abbrev primes_over.mk [P.IsMaximal] [P lies_over p] : primes_over p L := + ⟨P, (primes_over_mem p P).mpr ⟨inferInstance, inferInstance⟩⟩ + +theorem primes_over_card_ne_zero (L : Type*) [Field L] [NumberField L] [Algebra K L] : + Finset.card (primes_over p L) ≠ 0 := by + rcases exists_ideal_over_maximal_of_ringOfIntegers p L with ⟨P, hp⟩ + exact Finset.card_ne_zero_of_mem ((primes_over_mem p P).mpr hp) + +/-- Another form of the property `unique_lies_over`. -/ +theorem unique_primes_over_card_eq_one (P : Ideal (𝓞 L)) [hp : P unique_lies_over p] : + Finset.card (primes_over p L) = 1 := by + apply Nat.le_antisymm _ (Nat.one_le_iff_ne_zero.mpr (primes_over_card_ne_zero p L)) + simp only [Finset.card_le_one, primes_over_mem, and_imp] + intro a _ _ b _ _ + rw [hp.unique a, hp.unique b] + + + +variable {K L : Type*} [Field K] [Field L] [Algebra K L] {E : Type*} [Field E] + [Algebra K E] [Algebra E L] [IsScalarTower K E L] + (p : Ideal (𝓞 K)) (𝔓 : Ideal (𝓞 E)) (P : Ideal (𝓞 L)) + +theorem ideal_lies_over.trans [hp : 𝔓 lies_over p] [hP : P lies_over 𝔓] : P lies_over p where + over := by rw [hp.over, hP.over, comap_comap, ← IsScalarTower.algebraMap_eq] + +theorem ideal_lies_over_tower_bot [hp : P lies_over p] [hP : P lies_over 𝔓] : 𝔓 lies_over p where + over := by rw [hp.over, hP.over, comap_comap, ← IsScalarTower.algebraMap_eq] + +variable {K L : Type*} [Field K] [Field L] [NumberField L] [Algebra K L] {E : Type*} [Field E] + [Algebra K E] [Algebra E L] [IsScalarTower K E L] + (p : Ideal (𝓞 K)) (𝔓 : Ideal (𝓞 E)) (P : Ideal (𝓞 L)) + +omit [NumberField L] in +theorem ideal_unique_lies_over.trans [hp : 𝔓 unique_lies_over p] [hP : P unique_lies_over 𝔓] : + P unique_lies_over p := { ideal_lies_over.trans p 𝔓 P with + unique := fun Q _ _ ↦ + letI := ideal_lies_over_tower_bot p (idealUnder E Q) Q + letI := ideal_lies_over.mk (hp.unique (idealUnder E Q)).symm + hP.unique Q +} + +theorem ideal_unique_lies_over_tower_bot [hp : P unique_lies_over p] [hP : P lies_over 𝔓] : + 𝔓 unique_lies_over p := { ideal_lies_over_tower_bot p 𝔓 P with + unique := by + intro 𝔔 _ _ + rcases exists_ideal_over_maximal_of_ringOfIntegers 𝔔 L with ⟨Q, ⟨hqm ,hq⟩⟩ + letI := ideal_lies_over.trans p 𝔔 Q + letI := hp.unique Q + rw [hq.over, hp.unique Q, hP.over] +} + +theorem ideal_unique_lies_over_tower_top [𝔓.IsMaximal] [hP : P unique_lies_over p] + [𝔓 lies_over p] : P unique_lies_over 𝔓 where + over := by + rcases exists_ideal_over_maximal_of_ringOfIntegers 𝔓 L with ⟨Q, ⟨_ ,hq⟩⟩ + letI := ideal_lies_over.trans p 𝔓 Q + rw [← hP.unique Q, hq.over] + unique := fun Q _ _ ↦ + letI := ideal_lies_over.trans p 𝔓 Q + hP.unique Q + +variable {K L : Type*} [Field K] [Field L] [Algebra K L] +(p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) [P lies_over p] (E : IntermediateField K L) + +instance IntermediateField_ideal_lies_over : (idealUnder E P) lies_over p := + ideal_lies_over_tower_bot p (idealUnder E P) P + +theorem ideal_comap_intermediateField : p = idealUnder K (idealUnder E P) := + (IntermediateField_ideal_lies_over p P E).over + +variable {K L : Type*} [Field K] [Field L] [NumberField L] [Algebra K L] + (p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) [p.IsMaximal] [P.IsMaximal] + [P unique_lies_over p] (E : IntermediateField K L) + +instance IntermediateField_ideal_unique_lies_over : (idealUnder E P) unique_lies_over p := + ideal_unique_lies_over_tower_bot p (idealUnder E P) P + +end preparation + + + +section decomposition + +variable {K L : Type*} [Field K] [Field L] [Algebra K L] (p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) +[p.IsMaximal] [hpm : P.IsMaximal] [hp : P lies_over p] + +instance : P.LiesOver p where over := hp.over + +theorem inertiaDeg_pos {K L : Type*} [Field K] [NumberField K] [Field L] [NumberField L] + [Algebra K L] (p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) [p.IsMaximal] [P.IsMaximal] + [P lies_over p] : inertiaDeg (algebraMap (𝓞 K) (𝓞 L)) p P > 0 := by + rw [inertiaDeg_algebraMap] + exact Module.finrank_pos + + +/-! ### Galois group `Gal(K/L)` acts transitively on the set of all maximal ideals -/ + +open NumberField.RingOfIntegers + +theorem mapAlgEquiv_toAlgHom_toRingHom_eq_mapRingHom (σ : L ≃ₐ[K] L) : + (mapAlgEquiv σ).toAlgHom.toRingHom = mapRingHom σ := rfl + +theorem mapRingHom_one : mapRingHom (1 : L ≃ₐ[K] L) = RingHom.id (𝓞 L) := rfl + +theorem mapRingHom_symm_comp_mapRingHom (σ : L ≃ₐ[K] L) : (mapRingHom σ.symm).comp (mapRingHom σ) + = RingHom.id (𝓞 L) := + RingEquiv.symm_toRingHom_comp_toRingHom (mapRingEquiv σ) + +theorem mapRingHom_symm_apply_apply (σ : L ≃ₐ[K] L) (x : 𝓞 L) : + mapRingHom σ.symm (mapRingHom σ x) = x := + RingEquiv.symm_apply_apply (mapRingEquiv σ) x + +theorem mapRingHom_comp_mapRingHom_symm (σ : L ≃ₐ[K] L) : + (mapRingHom σ).comp (mapRingHom σ.symm) = RingHom.id (𝓞 L) := + RingEquiv.toRingHom_comp_symm_toRingHom (mapRingEquiv σ) + +theorem mapRingHom_apply_symm_apply (σ : L ≃ₐ[K] L) (x : 𝓞 L) : + mapRingHom σ (mapRingHom σ.symm x) = x := + RingEquiv.apply_symm_apply (mapRingEquiv σ) x + +theorem mapRingEquiv_symm_apply_apply (σ : L ≃ₐ[K] L) (x : 𝓞 L) : + mapRingEquiv σ.symm (mapRingEquiv σ x) = x := + RingEquiv.symm_apply_apply (mapRingEquiv σ) x + +theorem mapRingEquiv_apply_symm_apply (σ : L ≃ₐ[K] L) (x : 𝓞 L) : + mapRingEquiv σ (mapRingEquiv σ.symm x) = x := + RingEquiv.apply_symm_apply (mapRingEquiv σ) x + +/-- The `mapRingHom σ` will send a maximal ideal to a maximal ideal. -/ +instance mapRingHom_map.isMaximal (σ : L ≃ₐ[K] L) : (map (mapRingHom σ) P).IsMaximal := + Quotient.maximal_of_isField _ <| MulEquiv.isField _ (Field.toIsField ((𝓞 L) ⧸ P)) + (quotientEquiv P (map (mapRingHom σ) P) (mapAlgEquiv σ) rfl).symm.toMulEquiv + +-- Propsition 9.1 + +/-- The Galois group `Gal(K/L)` acts transitively on the set of all maximal ideals `P` of `𝓞 L` +lying above `p`, i.e., these prime ideals are all conjugates of each other. -/ +theorem isMaximal_conjugates {K L : Type*} [Field K] [NumberField K] [Field L] [NumberField L] + [Algebra K L] (p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) [hpm : P.IsMaximal] [hp : P lies_over p] + (Q : Ideal (𝓞 L)) [hqm : Q.IsMaximal] [hq : Q lies_over p] + [IsGalois K L] : ∃ σ : L ≃ₐ[K] L, map (mapRingHom σ) P = Q := by + by_contra hs + push_neg at hs + let s : Finset (L ≃ₐ[K] L) := Finset.univ + rcases Submodule.mem_sup.mp <| (eq_top_iff_one (Q ⊔ ∏ σ in s, map (mapRingHom σ) P)).mp <| + sup_prod_eq_top <| fun σ _ ↦ IsMaximal.coprime_of_ne hqm (mapRingHom_map.isMaximal P σ) + (hs σ).symm with ⟨x, hx, y, hy, hxy⟩ + let n : 𝓞 L := ∏ σ in s, (mapRingHom σ) x + have hnx : n = (algebraMap (𝓞 K) (𝓞 L)) (RingOfIntegers.norm K x) := + Subtype.val_inj.mp <| Eq.trans + (Submonoid.coe_finset_prod (integralClosure ℤ L).toSubmonoid (fun i ↦ (mapRingHom i) x) s) + (Algebra.norm_eq_prod_automorphisms K x.1).symm + have hnk : RingOfIntegers.norm K x ∈ idealUnder K P := by + rw [idealUnder, ← hp.over, hq.over] + apply mem_comap.mpr + rw [← hnx] + refine (span_singleton_le_iff_mem Q).mp ?_ + rw [← prod_span_singleton] + exact prod_le_inf.trans <| (@Finset.inf_le _ _ _ _ s (fun σ ↦ span {(mapRingHom σ) x}) _ + (@Finset.mem_univ (L ≃ₐ[K] L) _ 1)).trans (Iff.mpr (span_singleton_le_iff_mem Q) hx) + have hnp : n ∈ P := Eq.mpr (_root_.id (hnx ▸ Eq.refl (n ∈ P))) hnk + rcases IsPrime.prod_mem_iff.mp hnp with ⟨σ, _, hs⟩ + have hxp : x ∈ map (mapRingHom σ.symm) P := by + rw [← mapRingEquiv_symm_apply_apply σ x] + exact mem_map_of_mem (mapRingHom σ.symm) hs + have h := Ideal.add_mem (map (mapRingHom σ.symm) P) hxp <| + (prod_le_inf.trans (Finset.inf_le (Finset.mem_univ σ.symm))) hy + rw [hxy] at h + exact IsMaximal.ne_top (mapRingHom_map.isMaximal P σ.symm) ((eq_top_iff_one _).mpr h) + +theorem IsMaximal_conjugates' {K L : Type*} [Field K] [NumberField K] [Field L] [NumberField L] + [Algebra K L] {P : Ideal (𝓞 L)} [P.IsMaximal] {Q : Ideal (𝓞 L)} [Q.IsMaximal] + [IsGalois K L] (h : idealUnder K P = idealUnder K Q) : + ∃ σ : L ≃ₐ[K] L, map (mapRingHom σ) P = Q := + letI := ideal_lies_over.mk h + isMaximal_conjugates (idealUnder K P) P Q + + + +open UniqueFactorizationMonoid IsDedekindDomain + +/-- The function normalizedFactors commutes with the function `map (mapRingHom σ)`. -/ +theorem normalizedFactors_map_mapRingHom_commutes {K L : Type*} [Field K] [Field L] + [NumberField L] [Algebra K L] {I : Ideal (𝓞 L)} (hI : I ≠ ⊥) (σ : L ≃ₐ[K] L) : + normalizedFactors (map (mapRingHom σ) I) = + Multiset.map (map (mapRingHom σ)) (normalizedFactors I) := by + nth_rw 1 [← prod_normalizedFactors_eq_self hI] + have h := Multiset.prod_hom (normalizedFactors I) (mapHom (mapRingHom σ)) + simp only [mapHom_apply] at h + rw [← h, normalizedFactors_prod_of_prime] + intro q hq + rcases Multiset.mem_map.mp hq with ⟨p, hp, hpq⟩ + have : IsMaximal p := (prime_iff_isMaximal p).mp (prime_of_normalized_factor p hp) + rw [← hpq] + exact (prime_iff_isMaximal (map (mapRingHom σ) p)).mpr (mapRingHom_map.isMaximal p σ) + +/-- The image of an ideal under the algebraMap between ring of integers remains invariant +under the action of `mapRingHom σ`. -/ +theorem ideal_map_invariant_under_mapRingHom (p : Ideal (𝓞 K)) (σ : L ≃ₐ[K] L) : + (map (mapRingHom σ)) (map (algebraMap (𝓞 K) (𝓞 L)) p) = map (algebraMap (𝓞 K) (𝓞 L)) p := by + apply le_antisymm <| map_le_of_le_comap <| map_le_of_le_comap <| + fun _ h ↦ by simp only [← mapAlgEquiv_toAlgHom_toRingHom_eq_mapRingHom, + AlgEquiv.toAlgHom_eq_coe, AlgHom.toRingHom_eq_coe, mem_comap, RingHom.coe_coe, + AlgHom.commutes, mem_map_of_mem (algebraMap (𝓞 K) (𝓞 L)) h] + apply map_le_of_le_comap + intro x h + rw [mem_comap, map_map] + apply Set.mem_of_eq_of_mem _ (mem_map_of_mem ((mapRingHom σ).comp (algebraMap (𝓞 K) (𝓞 L))) h) + rw [mapRingHom, ← AlgEquiv.commutes (mapAlgEquiv σ) x] + rfl + +/-- The map induced by `mapRingHom σ` on the ideals of `𝓞 L` is injective. -/ +theorem mapRingHom_IdealMap.injective (σ : L ≃ₐ[K] L): Function.Injective (map (mapRingHom σ)) := + fun I J h ↦ by rw [← map_id I, ← mapRingHom_symm_comp_mapRingHom σ, ← map_map, h, map_map, + mapRingHom_symm_comp_mapRingHom σ, map_id] + +variable {K L : Type*} [Field K] [NumberField K] [Field L] [NumberField L] +[Algebra K L] (p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] + +/-- In the case of Galois extension, all the `ramificationIdx` are the same. -/ +theorem ramificationIdx_eq_of_isGalois (Q : Ideal (𝓞 L)) [hqm : Q.IsMaximal] [Q lies_over p] + [IsGalois K L] : ramificationIdx (algebraMap (𝓞 K) (𝓞 L)) p P = + ramificationIdx (algebraMap (𝓞 K) (𝓞 L)) p Q := by + classical + rcases isMaximal_conjugates p P Q with ⟨σ, hs⟩ + rw [ramificationIdx_eq_normalizedFactors_count (map_isMaximal_ne_bot p L) inferInstance + (ne_bot_ofIsMaximal P), ramificationIdx_eq_normalizedFactors_count (map_isMaximal_ne_bot p L) + (IsMaximal.isPrime hqm) (ne_bot_ofIsMaximal Q), ← hs] + nth_rw 2 [← ideal_map_invariant_under_mapRingHom p σ] + rw [normalizedFactors_map_mapRingHom_commutes (map_isMaximal_ne_bot p L) σ] + rw [Multiset.count_map_eq_count' _ _ (mapRingHom_IdealMap.injective σ) _] + +theorem ramificationIdx_eq_of_isGalois' [IsGalois K L] {P : Ideal (𝓞 L)} [P.IsMaximal] + {Q : Ideal (𝓞 L)} [hqm : Q.IsMaximal] (h : idealUnder K P = idealUnder K Q) : + ramificationIdx (algebraMap (𝓞 K) (𝓞 L)) (idealUnder K P) P = + ramificationIdx (algebraMap (𝓞 K) (𝓞 L)) (idealUnder K Q) Q := by + letI := ideal_lies_over.mk h + rw [← h] + exact ramificationIdx_eq_of_isGalois (idealUnder K P) P Q + +theorem idealUnder_invariant_under_mapRingHom {K L : Type*} [Field K] [Field L] [Algebra K L] + (p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) [hp : P lies_over p] (σ : L ≃ₐ[K] L) : + p = idealUnder K (map (mapRingHom σ) P) := by + ext x + rw [mem_comap, hp.over, mem_comap] + refine ⟨fun h ↦ Set.mem_of_eq_of_mem (by nth_rw 1 [← (mapAlgEquiv σ).commutes x]; rfl) + (mem_map_of_mem (mapRingHom σ) h), fun h ↦ ?_⟩ + have h := mem_map_of_mem (mapRingHom σ.symm) h + rw [map_map, mapRingHom_symm_comp_mapRingHom, map_id] at h + exact Set.mem_of_eq_of_mem (by nth_rw 1 [← (mapAlgEquiv σ.symm).commutes x]; rfl) h + +instance mapRingHom_map_lies_over (σ : L ≃ₐ[K] L) : (map (mapRingHom σ) P) lies_over p := + ⟨idealUnder_invariant_under_mapRingHom p P σ⟩ + +/-- The algebra equiv `((𝓞 L) ⧸ P) ≃ₐ[(𝓞 K) ⧸ p] ((𝓞 L) ⧸ map (mapRingHom σ) P)` +induced by an algebra equiv `σ : L ≃ₐ[K] L`. -/ +def residueField_mapAlgEquiv {P : Ideal (𝓞 L)} [P.IsMaximal] [P lies_over p] {Q : Ideal (𝓞 L)} + [Q.IsMaximal] [Q lies_over p] {σ : L ≃ₐ[K] L} (hs: map (mapRingHom σ) P = Q) : + ((𝓞 L) ⧸ P) ≃ₐ[(𝓞 K) ⧸ p] ((𝓞 L) ⧸ Q) := { + quotientEquiv P Q (mapAlgEquiv σ) (by rw [← hs]; rfl) with + commutes' := by + rintro ⟨x⟩ + exact congrArg (Ideal.Quotient.mk Q) (AlgEquiv.commutes (mapAlgEquiv σ) x) +} + +/-- In the case of Galois extension, all the `inertiaDeg` are the same. -/ +theorem inertiaDeg_eq_of_isGalois (Q : Ideal (𝓞 L)) [Q.IsMaximal] [Q lies_over p] [IsGalois K L] : + inertiaDeg (algebraMap (𝓞 K) (𝓞 L)) p P = inertiaDeg (algebraMap (𝓞 K) (𝓞 L)) p Q := by + rcases isMaximal_conjugates p P Q with ⟨σ, hs⟩ + rw [inertiaDeg_algebraMap, inertiaDeg_algebraMap] + exact LinearEquiv.finrank_eq (residueField_mapAlgEquiv p hs).toLinearEquiv + +/-- In the case of Galois extension, it can be seen from the Theorem `ramificationIdx_eq_of_IsGalois` +that all `ramificationIdx` are the same, which we define as the `ramificationIdx_of_isGalois`. -/ +@[irreducible] +noncomputable def ramificationIdx_of_isGalois (p : Ideal (𝓞 K)) [p.IsMaximal] + (L : Type*) [Field L] [NumberField L] [Algebra K L] : ℕ := + ramificationIdx (algebraMap (𝓞 K) (𝓞 L)) p <| + Classical.choose (exists_ideal_over_maximal_of_ringOfIntegers p L) + +/-- In the case of Galois extension, it can be seen from the Theorem `inertiaDeg_eq_of_IsGalois` +that all `inertiaDeg` are the same, which we define as the `inertiaDeg_of_isGalois`. -/ +@[irreducible] +noncomputable def inertiaDeg_of_isGalois (p : Ideal (𝓞 K)) [p.IsMaximal] + (L : Type*) [Field L] [NumberField L] [Algebra K L] : ℕ := + inertiaDeg (algebraMap (𝓞 K) (𝓞 L)) p <| + Classical.choose (exists_ideal_over_maximal_of_ringOfIntegers p L) + +/-- In the case of Galois extension, all ramification indices are equal to the +`ramificationIdx_of_isGalois`. This completes the property mentioned in our previous definition. -/ +theorem ramificationIdx_eq_ramificationIdx_of_isGalois [IsGalois K L] : + ramificationIdx (algebraMap (𝓞 K) (𝓞 L)) p P = ramificationIdx_of_isGalois p L := by + rcases Classical.choose_spec (exists_ideal_over_maximal_of_ringOfIntegers p L) with ⟨_, _⟩ + rw [ramificationIdx_of_isGalois] + exact ramificationIdx_eq_of_isGalois p P _ + +/-- In the case of Galois extension, all inertia degrees are equal to the `inertiaDeg_of_isGalois`. +This completes the property mentioned in our previous definition. -/ +theorem inertiaDeg_eq_inertiaDeg_of_isGalois [IsGalois K L] : + inertiaDeg (algebraMap (𝓞 K) (𝓞 L)) p P = inertiaDeg_of_isGalois p L := by + rcases Classical.choose_spec (exists_ideal_over_maximal_of_ringOfIntegers p L) with ⟨_, _⟩ + rw [inertiaDeg_of_isGalois] + exact inertiaDeg_eq_of_isGalois p P _ + +/-- The form of the **fundamental identity** in the case of Galois extension. -/ +theorem ramificationIdx_mul_inertiaDeg_of_isGalois (L : Type*) [Field L] [NumberField L] + [Algebra K L] [IsGalois K L] : + Finset.card (primes_over p L) * (ramificationIdx_of_isGalois p L * inertiaDeg_of_isGalois p L) = + Module.finrank K L := by + rw [← smul_eq_mul, ← Finset.sum_const] + rw [← sum_ramification_inertia (R := 𝓞 K) (S := 𝓞 L) p K L (ne_bot_ofIsMaximal p)] + apply Finset.sum_congr rfl + intro P hp + letI := ((primes_over_mem p P).mp hp).1 + letI := ((primes_over_mem p P).mp hp).2 + rw [ramificationIdx_eq_ramificationIdx_of_isGalois, inertiaDeg_eq_inertiaDeg_of_isGalois] + + + +-- Definition 9.2 +/-! ### decomposition Group -/ + +open MulAction + +/-- The `MulAction` of the Galois group `L ≃ₐ[K] L` on the set `primes_over p L`, +given by `σ ↦ (P ↦ σ P)`. -/ +instance Gal_MulAction_primes (L : Type*) [Field L] [NumberField L] [Algebra K L] : + MulAction (L ≃ₐ[K] L) (primes_over p L) where + smul σ Q := primes_over.mk p (map (mapRingHom σ) Q.1) + one_smul Q := by + show primes_over.mk p (map (mapRingHom (1 : L ≃ₐ[K] L)) Q.1) = Q + simp only [← Subtype.val_inj, mapRingHom_one, map_id] + mul_smul σ τ Q := by + show primes_over.mk p (map (mapRingHom (σ * τ)) Q.1) = + primes_over.mk p (map (mapRingHom σ) (primes_over.mk p (map (mapRingHom τ) Q.1)).1) + simp only [← Subtype.val_inj, map_map] + rfl + +theorem Gal_MulAction_primes_mk_coe (σ : L ≃ₐ[K] L) : + (σ • primes_over.mk p P).1 = map (mapRingHom σ) P := rfl + +/-- The decomposition group of `P` over `K`, is the stabilizer of `primes_over.mk p P` + under the action `Gal_MulAction_primes`. -/ +def decompositionGroup : Subgroup (L ≃ₐ[K] L) := stabilizer _ (primes_over.mk p P) + +/-- The `decompositionGroup` is consisting of all elements of the Galois group `L ≃ₐ[K] L` such +that keep `P` invariant. -/ +theorem decompositionGroup_mem (σ : L ≃ₐ[K] L) : + σ ∈ decompositionGroup p P ↔ map (mapRingHom σ) P = P := by + rw [decompositionGroup, mem_stabilizer_iff, ← Subtype.val_inj, Gal_MulAction_primes_mk_coe] + +open IntermediateField FiniteDimensional + +/-- The decomposition field of `P` over `K` is the fixed field of `decompositionGroup p P`. -/ +def decompositionField : IntermediateField K L := fixedField (decompositionGroup p P) + +/-- decompositionField is a Number Field. -/ +instance decompositionField_NumberField : NumberField (decompositionField p P) := + of_intermediateField (decompositionField p P) + +/-- The ideal equal to the intersection of `P` and `decompositionField p P`. -/ +abbrev decompositionIdeal : Ideal (𝓞 (decompositionField p P)) := + idealUnder (decompositionField p P) P + +instance decompositionIdeal.isMaximal : IsMaximal (decompositionIdeal p P) := + idealUnder.IsMaximal P + + + + +-- Proposition 9.3 + +open Classical + +theorem decompositionGroup_card_eq_ramificationIdx_mul_inertiaDeg [IsGalois K L] : + Fintype.card (decompositionGroup p P) = + ramificationIdx_of_isGalois p L * inertiaDeg_of_isGalois p L := by + apply mul_left_cancel₀ (primes_over_card_ne_zero p L) + have : Fintype (orbit (L ≃ₐ[K] L) (primes_over.mk p P)) := + Set.fintypeRange fun m ↦ m • primes_over.mk p P + rw [ramificationIdx_mul_inertiaDeg_of_isGalois, ← IsGalois.card_aut_eq_finrank, decompositionGroup] + rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (L ≃ₐ[K] L) (primes_over.mk p P)] + congr 1 + · rw [Fintype.card_of_finset' (@Finset.univ (primes_over p L) _), Finset.card_univ] + · exact (Fintype.card_coe (primes_over p L)).symm + · intro Q + simp only [Finset.univ_eq_attach, Finset.mem_attach, true_iff, MulAction.mem_orbit_iff] + rcases isMaximal_conjugates p P Q.1 with ⟨σ, hs⟩ + exact ⟨σ, by rw [← Subtype.val_inj, ← hs]; rfl⟩ + · congr + exact Subsingleton.elim (fun _ ↦ _) (fun _ ↦ _) + +theorem finrank_over_decompositionField_eq_ramificationIdx_mul_inertiaDeg + [IsGalois K L] : Module.finrank (decompositionField p P) L = + ramificationIdx_of_isGalois p L * inertiaDeg_of_isGalois p L := by + rw [decompositionField, finrank_fixedField_eq_card (decompositionGroup p P)] + rw [decompositionGroup_card_eq_ramificationIdx_mul_inertiaDeg p P] + +/-- `P` is the unique ideal lying over `decompositionIdeal p P`. -/ +theorem isMaximal_lies_over_decompositionideal_unique (Q : Ideal (𝓞 L)) [Q.IsMaximal] + [Q lies_over (decompositionIdeal p P)] [IsGalois K L] : Q = P := by + rcases isMaximal_conjugates (decompositionIdeal p P) P Q with ⟨σ, hs⟩ + let τ := (subgroup_equiv_aut (decompositionGroup p P)).toFun σ + have h : mapRingHom σ = mapRingHom τ.1 := rfl + rw [← hs, h, (decompositionGroup_mem p P τ.1).mp τ.2] + +/-- The instance form of `isMaximal_lies_over_decompositionideal_unique`. -/ +instance unique_lies_over_decompositionIdeal [IsGalois K L] : + P unique_lies_over (decompositionIdeal p P) := + { over_idealUnder P with unique := fun Q ↦ isMaximal_lies_over_decompositionideal_unique p P Q } + +/-- An alternative statement of `isMaximal_lies_over_decompositionideal_unique`. -/ +theorem primes_over_decompositionideal_card_eq_one [IsGalois K L] : + Finset.card (primes_over (decompositionIdeal p P) L) = 1 := + unique_primes_over_card_eq_one (decompositionIdeal p P) P + +private lemma ramificationIdx_and_inertiaDeg_of_decompositionIdeal [IsGalois K L] : + ramificationIdx_of_isGalois (decompositionIdeal p P) L = ramificationIdx_of_isGalois p L ∧ + inertiaDeg_of_isGalois (decompositionIdeal p P) L = inertiaDeg_of_isGalois p L := by + let Pz := idealUnder (decompositionField p P) P + let E := { x // x ∈ decompositionField p P } + have h := ramificationIdx_mul_inertiaDeg_of_isGalois Pz L + rw [primes_over_decompositionideal_card_eq_one p P, one_mul, + finrank_over_decompositionField_eq_ramificationIdx_mul_inertiaDeg p P] at h + have h0 := Nat.pos_of_ne_zero <| IsDedekindDomain.ramificationIdx_ne_zero + (map_isMaximal_ne_bot p L) inferInstance (map_le_of_le_comap (le_of_eq hp.over)) + have hr := Nat.le_of_dvd h0 <| Dvd.intro_left _ <| Eq.symm <| + ramificationIdx_algebra_tower (map_isMaximal_ne_bot Pz L) + (map_isMaximal_ne_bot p L) (map_le_iff_le_comap.mpr (le_of_eq rfl)) + have h0 : inertiaDeg (algebraMap (𝓞 K) (𝓞 L)) p P > 0 := inertiaDeg_pos p P + have hi := Nat.le_of_dvd h0 <| Dvd.intro_left _ <| Eq.symm <| inertiaDeg_algebra_tower + (ideal_comap_intermediateField p P (decompositionField p P)) (idealUnder_def E P) + rw [ramificationIdx_eq_ramificationIdx_of_isGalois Pz P, + ramificationIdx_eq_ramificationIdx_of_isGalois p P] at hr + rw [inertiaDeg_eq_inertiaDeg_of_isGalois Pz P, inertiaDeg_eq_inertiaDeg_of_isGalois p P] at hi + have hr0 := Nat.pos_of_ne_zero <| IsDedekindDomain.ramificationIdx_ne_zero + (map_isMaximal_ne_bot Pz L) inferInstance (map_le_of_le_comap (le_of_eq rfl)) + rw [inertiaDeg_eq_inertiaDeg_of_isGalois p P] at h0 + rw [ramificationIdx_eq_ramificationIdx_of_isGalois Pz P] at hr0 + exact (mul_eq_mul_iff_eq_and_eq_of_pos hr hi hr0 h0).mp h + +theorem ramificationIdx_of_decompositionIdeal [IsGalois K L] : + ramificationIdx_of_isGalois (decompositionIdeal p P) L = ramificationIdx_of_isGalois p L := + (ramificationIdx_and_inertiaDeg_of_decompositionIdeal p P).1 + +theorem inertiaDeg_of_decompositionIdeal [IsGalois K L] : + inertiaDeg_of_isGalois (decompositionIdeal p P) L = inertiaDeg_of_isGalois p L := + (ramificationIdx_and_inertiaDeg_of_decompositionIdeal p P).2 + +theorem ramificationIdx_of_decompositionideal_over_bot_eq_one [IsGalois K L] : ramificationIdx + (algebraMap (𝓞 K) (𝓞 (decompositionField p P))) p (decompositionIdeal p P) = 1 := by + let Pz := idealUnder (decompositionField p P) P + have h := ramificationIdx_algebra_tower (map_isMaximal_ne_bot Pz L) + (map_isMaximal_ne_bot p L) (map_le_iff_le_comap.mpr (le_of_eq rfl)) + rw [ramificationIdx_eq_ramificationIdx_of_isGalois Pz P, ramificationIdx_of_decompositionIdeal p P, + ← ramificationIdx_eq_ramificationIdx_of_isGalois p P] at h + nth_rw 1 [← one_mul (ramificationIdx (algebraMap (𝓞 K) (𝓞 L)) p P)] at h + exact mul_right_cancel₀ (IsDedekindDomain.ramificationIdx_ne_zero (map_isMaximal_ne_bot p L) + inferInstance (map_le_of_le_comap (le_of_eq hp.over))) h.symm + +/-- The residue class field corresponding to `decompositionField p P` is isomorphic to +residue class field corresponding to `p`. -/ +theorem inertiaDeg_of_decompositionideal_over_bot_eq_one [IsGalois K L] : inertiaDeg + (algebraMap (𝓞 K) (𝓞 (decompositionField p P))) p (decompositionIdeal p P) = 1 := by + have h := inertiaDeg_algebra_tower (ideal_comap_intermediateField p P (decompositionField p P)) + (idealUnder_def (decompositionField p P) P) + rw [inertiaDeg_eq_inertiaDeg_of_isGalois (idealUnder (decompositionField p P) P) P, + inertiaDeg_of_decompositionIdeal p P, ← inertiaDeg_eq_inertiaDeg_of_isGalois p P] at h + nth_rw 1 [← one_mul (inertiaDeg (algebraMap (𝓞 K) (𝓞 L)) p P)] at h + exact mul_right_cancel₀ (ne_of_gt (inertiaDeg_pos p P)) h.symm + + + +-- Proposition 9.4 +/-! ### inertia Group -/ + +/-- The residue class field of a number field is a finite field. -/ +noncomputable instance residue_field_instFintype : Finite ((𝓞 K) ⧸ p) := inferInstance + +/-- The extension between residue class fields of number fields is a Galois extension. -/ +instance extension_of_residue_fields_instIsGalois : IsGalois ((𝓞 K) ⧸ p) ((𝓞 L) ⧸ P) := + inferInstance + +/-- The inertia group of `P` over `K` is the subgorup of `L ≃ₐ[K] L` that consists of all +the `σ : L ≃ₐ[K] L` that are identity modulo `P`. -/ +def inertiaGroup (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L] + (P : Ideal (𝓞 L)) : Subgroup (L ≃ₐ[K] L) where + carrier := { σ | ∀ x : (𝓞 L), Ideal.Quotient.mk P (mapRingHom σ x) = Ideal.Quotient.mk P x } + mul_mem' := by + intro _ τ hs ht x + rw [← ht x, ← hs (mapRingHom τ x)] + rfl + one_mem' _ := rfl + inv_mem' := by + intro σ hs x + rw [show σ⁻¹ = σ.symm from rfl, ← hs (mapRingHom σ.symm x), mapRingHom_apply_symm_apply σ x] + +theorem inertiaGroup_le_decompositionGroup : inertiaGroup K P ≤ decompositionGroup p P := by + refine fun σ hs ↦ (decompositionGroup_mem p P σ).mpr <| + le_antisymm (map_le_of_le_comap (fun x hx ↦ ?_)) (fun x hx ↦ ?_) + · have h := add_mem (Ideal.Quotient.eq.mp (hs x)) hx + rw [sub_add_cancel] at h + exact mem_comap.mpr h + · rw [← mapRingEquiv_apply_symm_apply σ x] + have h := add_mem (Ideal.Quotient.eq.mp (((inertiaGroup K P).inv_mem hs) x)) hx + rw [sub_add_cancel] at h + exact mem_map_of_mem (mapRingHom σ) h + + + +section unique + +open FiniteDimensional IntermediateField Polynomial Module + +variable {K L : Type*} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] +(p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] + +/-- If `P` is the unique ideal lying over `p`, then `P` remains invariant under the action of `σ`. -/ +theorem mapRingHom_map_eq_of_unique_lies_over {K L : Type*} [Field K] [Field L] + [Algebra K L] (p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) [P.IsMaximal] + [hp : P unique_lies_over p] (σ : L ≃ₐ[K] L) : map (mapRingHom σ) P = P := + hp.unique (map (mapRingHom σ) P) + +/-- If `P` is the unique ideal lying over `p`, then the action of each element `σ` in `L ≃ₐ[K] L` +on the residue class field is an an automorphism of `(𝓞 L) ⧸ P` fixing `(𝓞 K) ⧸ p`, inducing a +homomorphism from `L ≃ₐ[K] L` to the Galois group `((𝓞 L) ⧸ P) ≃ₐ[(𝓞 K) ⧸ p] ((𝓞 L) ⧸ P)`. -/ +def residueGaloisHom : MonoidHom (L ≃ₐ[K] L) (((𝓞 L) ⧸ P) ≃ₐ[(𝓞 K) ⧸ p] ((𝓞 L) ⧸ P)) where + toFun σ := residueField_mapAlgEquiv p (mapRingHom_map_eq_of_unique_lies_over p P σ) + map_one' := by ext ⟨⟩; rfl + map_mul' _ _ := by ext ⟨⟩; rfl + +noncomputable abbrev powerBasis_of_residue : PowerBasis ((𝓞 K) ⧸ p) ((𝓞 L) ⧸ P) := + letI : Algebra.IsSeparable (𝓞 K ⧸ p) (𝓞 L ⧸ P) := IsGalois.to_isSeparable + Field.powerBasisOfFiniteOfSeparable ((𝓞 K) ⧸ p) ((𝓞 L) ⧸ P) + +theorem residueGaloisHom_surjective [hn : Normal K L] : + Function.Surjective (residueGaloisHom p P) := by + let F := 𝓞 K ⧸ p + let E := 𝓞 L ⧸ P + letI : Algebra E E := Algebra.id E + intro σ + have e : PowerBasis F E := powerBasis_of_residue p P + let β := (PowerBasis.liftEquiv e).toFun σ.toAlgHom + rcases Quotient.exists_rep e.gen with ⟨a, ha⟩ + let f : (𝓞 K)[X] := minpoly (𝓞 K) a + let fl : (𝓞 L)[X] := f.map (algebraMap (𝓞 K) (𝓞 L)) + let ϕp : (𝓞 K) →+* F := Ideal.Quotient.mk p + let ϕP : (𝓞 L) →+* E := Ideal.Quotient.mk P + have h : Quotient.mk (Submodule.quotientRel P) a = ϕP a := rfl + rw [h] at ha + have hai : IsIntegral (𝓞 K) a := IsIntegral.isIntegral a + have hm : f.Monic := minpoly.monic hai + have h0 : (fl.map ϕP) ≠ 0 := map_monic_ne_zero (Monic.map (algebraMap (𝓞 K) (𝓞 L)) hm) + have hbr : β.1 ∈ (fl.map ϕP).roots := by + have h : aeval e.gen (f.map ϕp) = ϕP (aeval a f) := by + rw [← ha] + exact (@map_aeval_eq_aeval_map _ _ _ F E _ _ _ _ _ ϕp ϕP rfl f a).symm + rw [minpoly.aeval, map_zero] at h + apply (mem_roots_iff_aeval_eq_zero h0).mpr + have hc : fl.map ϕP = (f.map ϕp).map (algebraMap F E) := by + rw [Polynomial.map_map, Polynomial.map_map] + rfl + have hbz := aeval_eq_zero_of_dvd_aeval_eq_zero (minpoly.dvd F e.gen h) β.2 + simp only [Equiv.toFun_as_coe, AlgEquiv.toAlgHom_eq_coe, PowerBasis.liftEquiv_apply_coe, + AlgHom.coe_coe, hc, aeval_map_algebraMap, ← hbz] + have hfe : (Polynomial.map (algebraMap (𝓞 K) K) f) = minpoly K a.1 := by + refine minpoly.eq_of_irreducible_of_monic + ((Monic.irreducible_iff_irreducible_map_fraction_map (minpoly.monic hai)).mp + (minpoly.irreducible hai)) ?_ (Monic.map (algebraMap (𝓞 K) K) (minpoly.monic hai)) + have h : a.1 = algebraMap (𝓞 L) L a := rfl + rw [h] + simp only [aeval_map_algebraMap, aeval_algebraMap_eq_zero_iff, minpoly.aeval, f] + have h : fl.roots.map ϕP = (fl.map ϕP).roots := by + have h := (natDegree_eq_card_roots' (hn.splits a.1)).symm + have hc : (algebraMap K L).comp (algebraMap (𝓞 K) K) = algebraMap (𝓞 K) L := rfl + have he := isIntegralClosure_root_card_eq_ofMonic (𝓞 L) L (minpoly.monic hai) + rw [← hfe, natDegree_map, Monic.natDegree_map (minpoly.monic hai), Polynomial.map_map, hc, ← he, + ← Monic.natDegree_map (minpoly.monic hai) (algebraMap (𝓞 K) (𝓞 L))] at h + exact roots_map_of_card_eq_natDegree h0 h + rw [← h] at hbr + rcases Multiset.mem_map.mp hbr with ⟨b, ⟨hbr, hb⟩⟩ + have h : aeval b.1 (minpoly K (AdjoinSimple.gen K a.1)) = 0 := by + have he : minpoly K (AdjoinSimple.gen K a.1) = minpoly K a.1 := by apply minpoly_eq + have h : b.1 = algebraMap (𝓞 L) L b := rfl + rw [he, ← hfe, h, aeval_map_algebraMap, aeval_algebraMap_eq_zero_iff, aeval_def, ← eval_map, + ← coe_aeval_eq_eval, (mem_roots_iff_aeval_eq_zero (map_monic_ne_zero hm)).mp hbr] + let ε := IntermediateField.adjoin.powerBasis (hn.isIntegral a.1) + use (ε.lift b.1 h).fieldRangeAlgEquiv.liftNormal L + refine AlgEquiv.coe_algHom_injective ((@PowerBasis.liftEquiv E _ F _ _ E _ _ e).injective ?_) + apply Subtype.val_inj.mp + rw [PowerBasis.liftEquiv_apply_coe, AlgHom.coe_coe] + simp only [← ha, Equiv.toFun_as_coe, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_coe] + show ϕP ((RingOfIntegers.mapAlgEquiv ((ε.lift b.1 h).fieldRangeAlgEquiv.liftNormal L)) a) = β.1 + rw [← hb] + congr + exact Subtype.val_inj.mp <| ((ε.lift b.1 h).fieldRangeAlgEquiv.liftNormal_commutes L + (AdjoinSimple.gen K a.1)).trans (ε.lift_gen b.1 h) + + + +-- Definition 9.5 + +open IsGalois + +/-- If `P` is the unique ideal lying over `p`, then the `inertiaGroup` is equal to the +kernel of the homomorphism `residueGaloisHom`. -/ +theorem inertiaGroup_eq_ker {K L : Type*} [Field K] [Field L] [Algebra K L] + (p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] : inertiaGroup K P = MonoidHom.ker (residueGaloisHom p P) := by + ext σ + rw [MonoidHom.mem_ker, AlgEquiv.ext_iff] + constructor + · rintro h ⟨x⟩ + nth_rw 2 [Submodule.Quotient.quot_mk_eq_mk] + rw [Quotient.mk_eq_mk, ← h x] + rfl + · intro h x + have h := h (Ideal.Quotient.mk P x) + rw [AlgEquiv.one_apply] at h + rw [← h] + rfl + +/-- If `P` is the unique ideal lying over `p`, then the `inertiaGroup K P` is a normal subgroup. -/ +theorem inertiaGroup_normal {K L : Type*} [Field K] [Field L] [Algebra K L] (p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) [p.IsMaximal] [P.IsMaximal] + [hp : P unique_lies_over p] : Subgroup.Normal (inertiaGroup K P) := by + rw [inertiaGroup_eq_ker p P] + exact MonoidHom.normal_ker (residueGaloisHom p P) + +noncomputable def aut_quoutient_inertiaGroup_equiv_residueField_aut [Normal K L] : + @MulEquiv ((L ≃ₐ[K] L) ⧸ (inertiaGroup K P)) (((𝓞 L) ⧸ P) ≃ₐ[(𝓞 K) ⧸ p] ((𝓞 L) ⧸ P)) + (letI := inertiaGroup_normal p P; inferInstance) _ := + letI := inertiaGroup_normal p P + (QuotientGroup.quotientMulEquivOfEq (inertiaGroup_eq_ker p P)).trans <| + QuotientGroup.quotientKerEquivOfSurjective _ (residueGaloisHom_surjective p P) + +/-- The intermediate field fixed by `inertiaGroup K P`. -/ +def inertiaField' (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L] + (P : Ideal (𝓞 L)) [P.IsMaximal] : IntermediateField K L := + fixedField (inertiaGroup K P) + +/-- `inertiaField' K P` is a Number Field. -/ +instance inertiaField_NumberField : NumberField (inertiaField' K P) := + of_intermediateField (inertiaField' K P) + +/-- The ideal equal to the intersection of `P` and `inertiaField' p P`. -/ +abbrev inertiaIdeal' (K : Type*) {L : Type*} [Field K] [Field L] + [Algebra K L] (P : Ideal (𝓞 L)) [P.IsMaximal] : Ideal (𝓞 (inertiaField' K P)) := + idealUnder (inertiaField' K P) P + +/-- `inertiaIdeal' p P` is a maximal Ideal. -/ +instance inertiaideal_IsMaxiaml : IsMaximal (inertiaIdeal' K P) := idealUnder.IsMaximal P + + + +-- Proposition 9.6 + +variable [IsGalois K L] + +/-- `(inertiaField' p P) / K` is a Galois extension. -/ +theorem inertiaField_isGalois_of_unique {K L : Type*} [Field K] [Field L] + [Algebra K L] [IsGalois K L] (p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) [p.IsMaximal] + [P.IsMaximal] [P unique_lies_over p] : IsGalois K (inertiaField' K P) := + letI := inertiaGroup_normal p P + of_fixedField_normal_subgroup (inertiaGroup K P) + +/-- The Galois group `Gal((inertiaField' p P) / K)` is isomorphic to the +Galois group `Gal((𝓞 L) ⧸ P) / (𝓞 K) ⧸ p)`. -/ +noncomputable def inertiaField_aut_equiv_ResidueField_aut : + ((inertiaField' K P) ≃ₐ[K] (inertiaField' K P)) ≃* (((𝓞 L) ⧸ P) ≃ₐ[(𝓞 K) ⧸ p] ((𝓞 L) ⧸ P)) := + letI := inertiaGroup_normal p P + (normal_aut_equiv_quotient (inertiaGroup K P)).trans <| + aut_quoutient_inertiaGroup_equiv_residueField_aut p P + +/-- The Galois group `Gal(L / (inertiaField' p P))` is isomorphic to `inertiaGroup K P`. -/ +def inertiaField_aut_tower_top_equiv_inertiaGroup_of_unique : + (L ≃ₐ[inertiaField' K P] L) ≃* inertiaGroup K P := subgroup_equiv_aut (inertiaGroup K P) + +/-- The extension degree `[L : K]` is equal to the product of the ramification index +and the inertia degree of `p` in `L`. -/ +theorem finrank_eq_ramificationIdx_mul_inertiaDeg (P : Ideal (𝓞 L)) + [P unique_lies_over p] : finrank K L = + ramificationIdx_of_isGalois p L * inertiaDeg_of_isGalois p L := by + have h := (ramificationIdx_mul_inertiaDeg_of_isGalois p L).symm + rw [unique_primes_over_card_eq_one p P, one_mul] at h + exact h + +/-- The extension degree `[inertiaField' p P : K]` is equal to the inertia degree of `p` in `L`. -/ +theorem finrank_bot_inertiaField_eq_inertiaDeg_of_unique : + finrank K (inertiaField' K P) = inertiaDeg_of_isGalois p L := by + letI := inertiaField_isGalois_of_unique p P + rw [← inertiaDeg_eq_inertiaDeg_of_isGalois p P, inertiaDeg, ← card_aut_eq_finrank] + rw [Fintype.card_of_bijective (inertiaField_aut_equiv_ResidueField_aut p P).bijective] + rw [card_aut_eq_finrank, dif_pos hp.over.symm] + +/-- The extension degree `[L : inertiaField' p P]` is equal to the +ramification index of `p` in `L`. -/ +theorem finrank_inertiaField_top_eq_ramificationIdx_of_unique : + finrank (inertiaField' K P) L = ramificationIdx_of_isGalois p L := by + have h : finrank K (inertiaField' K P) ≠ 0 := ne_of_gt finrank_pos + apply mul_left_cancel₀ h + rw [finrank_mul_finrank K (inertiaField' K P) L, finrank_eq_ramificationIdx_mul_inertiaDeg p P, + finrank_bot_inertiaField_eq_inertiaDeg_of_unique p P, mul_comm] + +theorem inertiaGroup_card_eq_ramificationIdx_of_unique : + Fintype.card (inertiaGroup K P) = ramificationIdx_of_isGalois p L := by + rw [← finrank_fixedField_eq_card, ← finrank_inertiaField_top_eq_ramificationIdx_of_unique p P] + rfl + +theorem inertiaGroup_inertiaideal_top (K : Type*) {L : Type*} [Field K] [NumberField K] [Field L] + [NumberField L] [Algebra K L] (P : Ideal (𝓞 L)) [P.IsMaximal] : + inertiaGroup (inertiaField' K P) P = ⊤ := by + refine (Subgroup.eq_top_iff' (inertiaGroup (inertiaField' K P) P)).mpr (fun σ x ↦ ?_) + let τ := (subgroup_equiv_aut (inertiaGroup K P)).toFun σ + have hst : (mapRingHom σ) x = (mapRingHom τ.1) x := rfl + rw [hst, τ.2 x] + +theorem inertiaDeg_over_inertiaideal_eq_one_of_unique (p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) + [P.IsMaximal] [P unique_lies_over p] : + inertiaDeg_of_isGalois (inertiaIdeal' K P) L = 1 := by + letI := ideal_unique_lies_over_tower_top p (inertiaIdeal' K P) P + letI := inertiaGroup_normal (inertiaIdeal' K P) P + rw [← inertiaDeg_eq_inertiaDeg_of_isGalois (inertiaIdeal' K P) P, inertiaDeg, dif_pos rfl] + rw [← card_aut_eq_finrank, ← Fintype.card_of_bijective <| MulEquiv.bijective <| + aut_quoutient_inertiaGroup_equiv_residueField_aut (inertiaIdeal' K P) P] + have hm := Subgroup.card_eq_card_quotient_mul_card_subgroup (inertiaGroup (inertiaField' K P) P) + nth_rw 1 [(Subgroup.card_eq_iff_eq_top (inertiaGroup (inertiaField' K P) P)).mpr <| + inertiaGroup_inertiaideal_top K P, ← one_mul (Nat.card (L ≃ₐ[inertiaField' K P] L))] at hm + simp only [Nat.card_eq_fintype_card] at hm + exact mul_right_cancel₀ Fintype.card_ne_zero hm.symm + +theorem ramificationIdx_over_inertiaideal_eq_ramificationIdx_of_unique : + ramificationIdx_of_isGalois (inertiaIdeal' K P) L = ramificationIdx_of_isGalois p L := by + letI := ideal_unique_lies_over_tower_top p (inertiaIdeal' K P) P + rw [← finrank_inertiaField_top_eq_ramificationIdx_of_unique p P] + rw [finrank_eq_ramificationIdx_mul_inertiaDeg (inertiaIdeal' K P) P] + rw [inertiaDeg_over_inertiaideal_eq_one_of_unique p P, mul_one] + +theorem ramificationIdx_below_inertiaideal_eq_one_of_unique : + ramificationIdx_of_isGalois p (inertiaField' K P) = 1 := by + let Pt := idealUnder (inertiaField' K P) P + letI := inertiaField_isGalois_of_unique p P + have h := ramificationIdx_algebra_tower (map_isMaximal_ne_bot Pt L) + (map_isMaximal_ne_bot p L) (map_le_iff_le_comap.mpr (le_of_eq rfl)) + nth_rw 1 [ramificationIdx_eq_ramificationIdx_of_isGalois Pt P, + ramificationIdx_over_inertiaideal_eq_ramificationIdx_of_unique p P, + ← ramificationIdx_eq_ramificationIdx_of_isGalois p P, + ← one_mul (ramificationIdx (algebraMap (𝓞 K) (𝓞 L)) p P), + ramificationIdx_eq_ramificationIdx_of_isGalois p Pt] at h + exact mul_right_cancel₀ (IsDedekindDomain.ramificationIdx_ne_zero (map_isMaximal_ne_bot p L) + (IsMaximal.isPrime inferInstance) (map_le_of_le_comap (le_of_eq hp.over))) h.symm + +theorem inertiaDeg_below_inertiaideal_eq_inertiaDeg_of_unique : + inertiaDeg_of_isGalois p (inertiaField' K P) = inertiaDeg_of_isGalois p L := by + letI := inertiaField_isGalois_of_unique p P + have h := inertiaDeg_algebra_tower (ideal_comap_intermediateField p P (inertiaField' K P)) + (idealUnder_def (inertiaField' K P) P) + nth_rw 1 [inertiaDeg_eq_inertiaDeg_of_isGalois (inertiaIdeal' K P) P, + inertiaDeg_over_inertiaideal_eq_one_of_unique p P, mul_one] at h + simp_rw [inertiaDeg_eq_inertiaDeg_of_isGalois] at h + exact h.symm + +end unique + + + +section inertia + +/- TODO : The genral version of `inertiaField_aut_equiv_ResidueField_aut`, i.e., +`((inertiaField p P) ≃ₐ[decompositionField p P] (inertiaField p P))` is isomorphic to +`(((𝓞 L) ⧸ P) ≃ₐ[(𝓞 K) ⧸ p] ((𝓞 L) ⧸ P))`. -/ + +open IntermediateField FiniteDimensional Classical + +variable {K L : Type*} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] +(p : Ideal (𝓞 K)) (P : Ideal (𝓞 L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] + +theorem inertiaGroup_eq : + Subgroup.map (subgroup_equiv_aut (decompositionGroup p P)).symm.toMonoidHom + ((inertiaGroup K P).subgroupOf (decompositionGroup p P)) = + inertiaGroup (decompositionField p P) P := by + ext σ + rw [Subgroup.mem_map] + refine ⟨fun ⟨τ, ht, he⟩ x ↦ by rw [← he, ← Subgroup.mem_subgroupOf.mp ht x]; rfl, fun hs ↦ ?_⟩ + refine ⟨(subgroup_equiv_aut (decompositionGroup p P)).toFun σ, fun x ↦ by rw [← hs x]; rfl, ?_⟩ + rw [MulEquiv.toEquiv_eq_coe] + simp only [Equiv.toFun_as_coe, MulEquiv.coe_toEquiv, MulEquiv.coe_toMonoidHom, + MulEquiv.symm_apply_apply] + +def inertiaGroup_equiv : inertiaGroup (decompositionField p P) P ≃* inertiaGroup K P := + (MulEquiv.subgroupCongr (inertiaGroup_eq p P)).symm.trans <| + ((subgroup_equiv_aut (decompositionGroup p P)).symm.subgroupMap + ((inertiaGroup K P).subgroupOf (decompositionGroup p P))).symm.trans <| + (Subgroup.subgroupOfEquivOfLe (inertiaGroup_le_decompositionGroup p P)) + +/-- The intertia field of `P` over `K` is the intermediate field of `L / decompositionField p P` +fixed by the inertia group pf `P` over `K`. -/ +def inertiaField : IntermediateField (decompositionField p P) L := + fixedField (inertiaGroup (decompositionField p P) P) + +/-- The ideal equal to the intersection of `P` and `inertiaField p P`. -/ +abbrev inertiaIdeal : Ideal (𝓞 (inertiaField p P)) := idealUnder (inertiaField p P) P + +/-- `(inertiaField p P) / (decompositionField p P)` is a Galois extension. -/ +instance inertiaField_isGalois [IsGalois K L] : IsGalois (decompositionField p P) (inertiaField p P) := + inertiaField_isGalois_of_unique (decompositionIdeal p P) P + +/-- The Galois group `Gal(L / (inertiaField p P))` is isomorphic to `inertiaGroup K P`. -/ +def inertiaField_aut_tower_top_equiv_inertiaGroup : + (L ≃ₐ[inertiaField p P] L) ≃* inertiaGroup K P := + (subgroup_equiv_aut (inertiaGroup (decompositionField p P) P)).trans (inertiaGroup_equiv p P) + +/-- The extension degree `[inertiaField p P : K]` is equal to the inertia degree of `p` in `L`. -/ +theorem finrank_bot_inertiaField_eq_inertiaDeg [IsGalois K L] : + Module.finrank (decompositionField p P) (inertiaField p P) = inertiaDeg_of_isGalois p L := by + rw [← inertiaDeg_of_decompositionIdeal p P] + exact finrank_bot_inertiaField_eq_inertiaDeg_of_unique (decompositionIdeal p P) P + +/-- The extension degree `[L : inertiaField p P]` is equal to the +ramification index of `p` in `L`. -/ +theorem finrank_inertiaField_top_eq_ramificationIdx [IsGalois K L] : + Module.finrank (inertiaField p P) L = ramificationIdx_of_isGalois p L := by + rw [← ramificationIdx_of_decompositionIdeal p P] + exact finrank_inertiaField_top_eq_ramificationIdx_of_unique (decompositionIdeal p P) P + +theorem inertiaGroup_card_eq_ramificationIdx [IsGalois K L] : + Fintype.card (inertiaGroup K P) = ramificationIdx_of_isGalois p L := by + rw [← ramificationIdx_of_decompositionIdeal p P] + rw [Fintype.card_of_bijective (inertiaGroup_equiv p P).symm.bijective] + rw [inertiaGroup_card_eq_ramificationIdx_of_unique (decompositionIdeal p P) P] + +theorem inertiaDeg_over_inertiaideal_eq_one [IsGalois K L] : + inertiaDeg_of_isGalois (inertiaIdeal p P) L = 1 := + inertiaDeg_over_inertiaideal_eq_one_of_unique (decompositionIdeal p P) P + +theorem ramificationIdx_over_inertiaideal_eq_ramificationIdx [IsGalois K L] : + ramificationIdx_of_isGalois (inertiaIdeal p P) L = ramificationIdx_of_isGalois p L := by + rw [← ramificationIdx_of_decompositionIdeal p P] + exact ramificationIdx_over_inertiaideal_eq_ramificationIdx_of_unique (decompositionIdeal p P) P + +theorem ramificationIdx_below_inertiaideal_eq_one [IsGalois K L] : + ramificationIdx_of_isGalois (decompositionIdeal p P) (inertiaField p P) = 1 := + ramificationIdx_below_inertiaideal_eq_one_of_unique (decompositionIdeal p P) P + +theorem inertiaDeg_below_inertiaideal_eq_inertiaDeg [IsGalois K L] : + inertiaDeg_of_isGalois (decompositionIdeal p P) (inertiaField p P) = + inertiaDeg_of_isGalois p L := by + rw [← inertiaDeg_of_decompositionIdeal p P] + exact inertiaDeg_below_inertiaideal_eq_inertiaDeg_of_unique (decompositionIdeal p P) P + +noncomputable def inertiaField_decompositionField_aut_equiv_ResidueField_aut [IsGalois K L] : + ((inertiaField p P) ≃ₐ[decompositionField p P] (inertiaField p P)) ≃* + (((𝓞 L) ⧸ P) ≃ₐ[(𝓞 K) ⧸ p] ((𝓞 L) ⧸ P)) := + letI : IsScalarTower (𝓞 K ⧸ p) (𝓞 (decompositionField p P) ⧸ decompositionIdeal p P) (𝓞 L ⧸ P) := + IsScalarTower.of_algebraMap_eq (by rintro ⟨_⟩; rfl) + have h : Module.finrank ((𝓞 K) ⧸ p) ((𝓞 (decompositionField p P)) ⧸ (decompositionIdeal p P)) = 1 := by + rw [← inertiaDeg_algebraMap] + exact inertiaDeg_of_decompositionideal_over_bot_eq_one p P + (inertiaField_aut_equiv_ResidueField_aut (decompositionIdeal p P) P).trans <| + aut_equiv_of_finrank_eq_one _ h + +end inertia diff --git a/GaloisRamification/ToMathlib.lean b/GaloisRamification/ToMathlib.lean new file mode 100644 index 0000000..5dd66b3 --- /dev/null +++ b/GaloisRamification/ToMathlib.lean @@ -0,0 +1,133 @@ +/- +Copyright (c) 2024 Yongle Hu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yongle Hu +-/ +import Mathlib.FieldTheory.PurelyInseparable +import Mathlib.NumberTheory.NumberField.Basic +import Mathlib.RingTheory.Valuation.ValuationRing + +import GaloisRamification.ToMathlib.Finite +import GaloisRamification.ToMathlib.FractionRing +import GaloisRamification.ToMathlib.Normal +import GaloisRamification.ToMathlib.restrictScalarsHom +import GaloisRamification.ToMathlib.separableClosure + +set_option autoImplicit false + +open Algebra + +open scoped BigOperators + +/-! ### Preliminary -/ + +section Galois + +open IntermediateField AlgEquiv QuotientGroup + +variable {K E L : Type*} [Field K] [Field E] [Field L] [Algebra K E] [Algebra K L] [Algebra E L] + [IsScalarTower K E L] + +/-- The `AlgEquiv` induced by an `AlgHom` from the domain of definition to the `fieldRange`. -/ +noncomputable def AlgHom.fieldRangeAlgEquiv (σ : E →ₐ[K] L) : + E ≃ₐ[K] σ.fieldRange where + toFun x := ⟨σ x, by simp only [AlgHom.mem_fieldRange, exists_apply_eq_apply]⟩ + invFun y := Classical.choose (AlgHom.mem_fieldRange.mp y.2) + left_inv x := σ.toRingHom.injective (Classical.choose_spec (AlgHom.mem_fieldRange.mp ⟨x, rfl⟩)) + right_inv y := Subtype.val_inj.mp (Classical.choose_spec (mem_fieldRange.mp y.2)) + map_mul' x y := Subtype.val_inj.mp (σ.toRingHom.map_mul x y) + map_add' x y := Subtype.val_inj.mp (σ.toRingHom.map_add x y) + commutes' x := Subtype.val_inj.mp (commutes σ x) + +variable [FiniteDimensional K L] + +/-- If `H` is a subgroup of `Gal(L/K)`, then `Gal(L / fixedField H)` is isomorphic to `H`. -/ +def IntermediateField.subgroup_equiv_aut (H : Subgroup (L ≃ₐ[K] L)) : + (L ≃ₐ[fixedField H] L) ≃* H where + toFun ϕ := ⟨ϕ.restrictScalars _, le_of_eq (fixingSubgroup_fixedField H) ϕ.commutes⟩ + invFun ϕ := { toRingEquiv (ϕ : L ≃ₐ[K] L) with + commutes' := (ge_of_eq (fixingSubgroup_fixedField H)) ϕ.mem } + left_inv _ := by ext; rfl + right_inv _ := by ext; rfl + map_mul' _ _ := by ext; rfl + +variable {K L : Type*} [Field K] [Field L] [Algebra K L] {E : IntermediateField K L} + +/-- If `H` is a normal Subgroup of `Gal(L / K)`, then `fixedField H` is Galois over `K`. -/ +instance of_fixedField_normal_subgroup [IsGalois K L] + (H : Subgroup (L ≃ₐ[K] L)) [hn : Subgroup.Normal H] : IsGalois K (fixedField H) where + to_isSeparable := Algebra.isSeparable_tower_bot_of_isSeparable K (fixedField H) L + to_normal := by + apply normal_iff_forall_map_le'.mpr + intro σ x ⟨a, ha, hax⟩ τ + rw [← hax] + calc _ = (σ * σ⁻¹ * τ.1 * σ) a := by rw [mul_inv_cancel]; rfl + _ = _ := by nth_rw 2 [← ha ⟨_ , (Subgroup.Normal.conj_mem hn τ.1 τ.2 σ⁻¹)⟩]; rfl + +/-- If `H` is a normal Subgroup of `Gal(L/K)`, then `Gal(fixedField H/K)` is isomorphic to +`Gal(L/K)⧸H`. -/ +noncomputable def IsGalois.normal_aut_equiv_quotient [FiniteDimensional K L] [IsGalois K L] + (H : Subgroup (L ≃ₐ[K] L)) [Subgroup.Normal H] : + ((fixedField H) ≃ₐ[K] (fixedField H)) ≃* (L ≃ₐ[K] L) ⧸ H := sorry/- by + apply MulEquiv.symm <| (quotientMulEquivOfEq ((fixingSubgroup_fixedField H).symm.trans _)).trans + <| quotientKerEquivOfSurjective (restrictNormalHom (fixedField H)) <| + restrictNormalHom_surjective L + ext σ + apply (((mem_fixingSubgroup_iff (L ≃ₐ[K] L)).trans ⟨fun h ⟨x, hx⟩ ↦ Subtype.val_inj.mp <| + (restrictNormal_commutes σ (fixedField H) ⟨x, hx⟩).trans (h x hx) , _⟩).trans + AlgEquiv.ext_iff.symm).trans (MonoidHom.mem_ker (restrictNormalHom (fixedField H))).symm + intro h x hx + dsimp + have hs : ((restrictNormalHom (fixedField H)) σ) ⟨x, hx⟩ = σ x := + restrictNormal_commutes σ (fixedField H) ⟨x, hx⟩ + rw [← hs] + exact Subtype.val_inj.mpr (h ⟨x, hx⟩) -/ + +end Galois + + + +namespace Polynomial + +variable {R : Type*} (S L : Type*) [CommRing R] [CommRing S] [IsDomain S] [CommRing L] [IsDomain L] +[Algebra R L] [Algebra S L] [Algebra R S] [IsScalarTower R S L] [IsIntegralClosure S R L] + + +open Multiset + +/-- If `L` be an extension of `R`, then for a monic polynomial `p : R[X]`, the roots of `p`in `L` +are equal to the roots of `p` in the integral closure of `R` in `L`. -/ +theorem isIntegralClosure_root_eq_ofMonic {p : R[X]} (hp : p.Monic): + (map (algebraMap R S) p).roots.map (algebraMap S L) = (map (algebraMap R L) p).roots := by + classical + ext x + by_cases hx : ∃ y : S, algebraMap S L y = x + · rcases hx with ⟨y, h⟩ + have hi : Function.Injective (algebraMap S L) := IsIntegralClosure.algebraMap_injective S R L + rw [← h, count_map_eq_count' _ _ hi _, count_roots, count_roots, + IsScalarTower.algebraMap_eq R S L, ← map_map, ← eq_rootMultiplicity_map hi] + · have h : count x ((p.map (algebraMap R S)).roots.map (algebraMap S L)) = 0 := by + simp only [mem_map, mem_roots', ne_eq, IsRoot.def, Subtype.exists, not_exists, + not_and, and_imp, count_eq_zero] + intro y _ _ h + exact hx ⟨y, h⟩ + rw [h] + exact Decidable.byContradiction fun h ↦ hx <| IsIntegralClosure.isIntegral_iff.mp + ⟨p, hp, (eval₂_eq_eval_map (algebraMap R L)).trans <| + (mem_roots (hp.map (algebraMap R L)).ne_zero).1 (count_ne_zero.mp (Ne.symm h))⟩ + +/-- If `L` be an extension of `R`, then for a monic polynomial `p : R[X]`, the number of roots +of `p` in `L` is equal to the number of roots of `p` in the integral closure of `R` in `L`. -/ +theorem isIntegralClosure_root_card_eq_ofMonic {p : R[X]} (hp : p.Monic) : + card (map (algebraMap R S) p).roots = card (map (algebraMap R L) p).roots := by + rw [← isIntegralClosure_root_eq_ofMonic S L hp, card_map] + +/-- A variant of the theorem `Polynomial.roots_map_of_injective_of_card_eq_natDegree` that + replaces the injectivity condition with the condition `Polynomial.map f p ≠ 0`. -/ +theorem roots_map_of_card_eq_natDegree {A B : Type*} [CommRing A] [CommRing B] + [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} (h : p.map f ≠ 0) + (hroots : card p.roots = p.natDegree) : p.roots.map f = (map f p).roots := by + apply eq_of_le_of_card_le (map_roots_le h) + simpa only [card_map, hroots] using (card_roots' (map f p)).trans (natDegree_map_le f p) + +end Polynomial diff --git a/GaloisRamification/ToMathlib/Finite.lean b/GaloisRamification/ToMathlib/Finite.lean new file mode 100644 index 0000000..618c4f8 --- /dev/null +++ b/GaloisRamification/ToMathlib/Finite.lean @@ -0,0 +1,60 @@ +/- +Copyright (c) 2024 Yongle Hu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yongle Hu +-/ +import Mathlib.NumberTheory.NumberField.Basic + +section + +open Ideal + +attribute [local instance] Ideal.Quotient.field in +/-- If `p` is a non-zero ideal of the `ℤ`, then `ℤ ⧸ p` is finite. -/ +theorem Int.Quotient.finite_of_ne_bot {I : Ideal ℤ} (h : I ≠ ⊥) : Finite (ℤ ⧸ I) := by + have equiv := Int.quotientSpanEquivZMod (Submodule.IsPrincipal.generator I) + rw [span_singleton_generator I] at equiv + haveI : NeZero (Submodule.IsPrincipal.generator I).natAbs := ⟨fun eq ↦ + h ((Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero I).mpr (Int.natAbs_eq_zero.mp eq))⟩ + exact Finite.of_equiv (ZMod (Submodule.IsPrincipal.generator I).natAbs) equiv.symm + +/-- In particular, if `p` is a maximal ideal of the `ℤ`, then `ℤ ⧸ p` is a finite field. -/ +instance Int.Quotient.finite_of_is_maxiaml (p : Ideal ℤ) [hpm : p.IsMaximal] : + Finite (ℤ ⧸ p) := + finite_of_ne_bot (Ring.ne_bot_of_isMaximal_of_not_isField hpm Int.not_isField) + +/- #check Module.finite_of_finite +#check FiniteDimensional.fintypeOfFintype +def Module.Finite.finiteOfFinite {R M : Type*} [CommRing R] [Finite R] [AddCommMonoid M] [Module R M] + [Module.Finite R M] : Finite M := by + have := exists_fin' R M --exact .of_surjective f hf + sorry -/ + +variable {R : Type*} [CommRing R] [h : Module.Finite ℤ R] + +theorem Ideal.Quotient.finite_of_module_finite_int {I : Ideal R} (hp : I ≠ ⊥) : Finite (R ⧸ I) := sorry + +-- `NoZeroSMulDivisors` can be removed +instance Ideal.Quotient.finite_of_module_finite_int_of_isMaxiaml [NoZeroSMulDivisors ℤ R] [IsDomain R] + (p : Ideal R) [hpm : p.IsMaximal] : Finite (R ⧸ p) := + Ideal.Quotient.finite_of_module_finite_int <| Ring.ne_bot_of_isMaximal_of_not_isField hpm <| + fun hf => Int.not_isField <| + (Algebra.IsIntegral.isField_iff_isField (NoZeroSMulDivisors.algebraMap_injective ℤ R)).mpr hf + +end + +namespace NumberField + +variable {K : Type*} [Field K] [NumberField K] + +/-- For any nonzero ideal `I` of `𝓞 K`, `(𝓞 K) ⧸ I` has only finite elements. + Note that if `I` is maximal, then `Finite ((𝓞 K) ⧸ I)` can be obtained by `inferInstance`. -/ +theorem quotientFiniteOfNeBot {I : Ideal (𝓞 K)} (h : I ≠ ⊥) : Finite ((𝓞 K) ⧸ I) := + Ideal.Quotient.finite_of_module_finite_int h + +example (p : Ideal (𝓞 K)) [p.IsMaximal] : Finite ((𝓞 K) ⧸ p) := inferInstance + +/- instance quotientFiniteOfIsMaxiaml (p : Ideal (𝓞 K)) [hpm : p.IsMaximal] : Finite ((𝓞 K) ⧸ p) := + quotientFiniteOfNeBot (Ring.ne_bot_of_isMaximal_of_not_isField hpm (RingOfIntegers.not_isField K)) -/ + +end NumberField diff --git a/GaloisRamification/ToMathlib/FractionRing.lean b/GaloisRamification/ToMathlib/FractionRing.lean new file mode 100644 index 0000000..1b72d47 --- /dev/null +++ b/GaloisRamification/ToMathlib/FractionRing.lean @@ -0,0 +1,13 @@ +/- +Copyright (c) 2024 Yongle Hu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yongle Hu +-/ +import Mathlib.LinearAlgebra.FiniteDimensional.Defs +import Mathlib.RingTheory.Localization.FractionRing + +attribute [local instance] FractionRing.liftAlgebra + +instance {A B : Type*} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] + [Module.Finite A B] [NoZeroSMulDivisors A B] : + FiniteDimensional (FractionRing A) (FractionRing B) := sorry diff --git a/GaloisRamification/ToMathlib/Normal.lean b/GaloisRamification/ToMathlib/Normal.lean new file mode 100644 index 0000000..5f57b9a --- /dev/null +++ b/GaloisRamification/ToMathlib/Normal.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2024 Yongle Hu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yongle Hu +-/ +import Mathlib.FieldTheory.PurelyInseparable +import Mathlib.NumberTheory.NumberField.Basic +import Mathlib.RingTheory.Valuation.ValuationRing + +attribute [local instance] Ideal.Quotient.field + +variable {A B : Type*} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] + (p : Ideal A) (P : Ideal B) [p.IsMaximal] [P.IsMaximal] [P.LiesOver p] + (K L : Type*) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] + [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Normal K L] + +example : Normal (A ⧸ p) (B ⧸ P) := sorry diff --git a/GaloisRamification/ToMathlib/restrictScalarsHom.lean b/GaloisRamification/ToMathlib/restrictScalarsHom.lean new file mode 100644 index 0000000..b94c9af --- /dev/null +++ b/GaloisRamification/ToMathlib/restrictScalarsHom.lean @@ -0,0 +1,29 @@ +/- +Copyright (c) 2024 Yongle Hu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yongle Hu +-/ +import Mathlib.Algebra.Algebra.Subalgebra.Tower +import Mathlib.LinearAlgebra.Dimension.Finrank + +variable (R S A : Type*) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] + [Algebra R A] [IsScalarTower R S A] + +def AlgEquiv.restrictScalarsHom : (A ≃ₐ[S] A) →* (A ≃ₐ[R] A) where + toFun f := AlgEquiv.restrictScalars R f + map_one' := rfl + map_mul' _ _ := rfl + +theorem AlgEquiv.restrictScalarsHom_injective : Function.Injective (AlgEquiv.restrictScalarsHom R S A) := + AlgEquiv.restrictScalars_injective R + +theorem AlgEquiv.restrictScalarsHom_bot_surjective : + Function.Surjective (AlgEquiv.restrictScalarsHom R (⊥ : Subalgebra R S) S) := sorry + +noncomputable def subalgebra_bot_aut_equiv : (S ≃ₐ[(⊥ : Subalgebra R S)] S) ≃* (S ≃ₐ[R] S) := + MulEquiv.ofBijective _ + ⟨AlgEquiv.restrictScalarsHom_injective R _ S, AlgEquiv.restrictScalarsHom_bot_surjective R S⟩ + +noncomputable def aut_equiv_of_finrank_eq_one {R S : Type*} (A : Type*) [CommSemiring R] [CommRing S] + [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] + (h : Module.finrank R S = 1) : (A ≃ₐ[S] A) ≃* (A ≃ₐ[R] A) := sorry diff --git a/GaloisRamification/ToMathlib/separableClosure.lean b/GaloisRamification/ToMathlib/separableClosure.lean new file mode 100644 index 0000000..4645bb1 --- /dev/null +++ b/GaloisRamification/ToMathlib/separableClosure.lean @@ -0,0 +1,33 @@ +/- +Copyright (c) 2024 Yongle Hu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yongle Hu +-/ +import Mathlib.FieldTheory.PurelyInseparable + +namespace separableClosure + +variable (K L : Type*) [Field K] [Field L] [Algebra K L] [Normal K L] + +#check IsPurelyInseparable.injective_comp_algebraMap + +#check instUniqueAlgHomOfIsPurelyInseparable + +#check separableClosure.isPurelyInseparable + +theorem restrictNormalHom_injective : Function.Injective + (AlgEquiv.restrictNormalHom (F := K) (K₁ := L) (separableClosure K L)) := by + sorry + +noncomputable def restrictNormalEquiv : (L ≃ₐ[K] L) ≃* + (separableClosure K L) ≃ₐ[K] (separableClosure K L) := + MulEquiv.ofBijective _ + ⟨restrictNormalHom_injective K L, AlgEquiv.restrictNormalHom_surjective L⟩ + +example (e : PowerBasis K (separableClosure K L)) (σ τ : L ≃ₐ[K] L) (h : σ e.gen = τ e.gen) : σ = τ := by + sorry + +example [FiniteDimensional K L] : ∃ x : L, ∀ σ τ : L ≃ₐ[K] L, σ x = τ x → σ = τ := by + sorry + +end separableClosure diff --git a/README.md b/README.md new file mode 100644 index 0000000..41ade07 --- /dev/null +++ b/README.md @@ -0,0 +1 @@ +# GaloisRamification \ No newline at end of file diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..e16da4e --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,125 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "dc72dcdb8e97b3c56bd70f06f043ed2dee3258e6", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "9ac12945862fa39eab7795c2f79bb9aa0c8e332c", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "baa65c6339a56bd22b7292aa4511c54b3cc7a6af", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.43", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "0ea83a676d288220ba227808568cbb80fe43ace0", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "7bedaed1ef024add1e171cc17706b012a9a37802", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "e91cdbcf5a387801a6225b41b0056c63206a9f7f", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "6d2e06515f1ed1f74208d5a1da3a9cc26c60a7a0", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "85e1e7143dd4cfa2b551826c27867bada60858e8", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/doc-gen4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "d36b7fd4c730cae8a3a8edfe98beb34ef0fc6e0a", + "name": "«doc-gen4»", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean"}], + "name": "GaloisRamification", + "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000..66735ef --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,20 @@ +import Lake +open Lake DSL + +package "GaloisRamification" where + -- Settings applied to both builds and interactive editing + leanOptions := #[ + ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b` + ] + -- add any additional package configuration options here + version := v!"0.1.0" + +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git" + +lean_lib «GaloisRamification» where + -- add library configuration options here + +meta if get_config? env = some "dev" then +require «doc-gen4» from git + "https://github.com/leanprover/doc-gen4" @ "main" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..eff86fd --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.13.0-rc3