init

.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

.gitignore

@@ -0,0 +1 @@
+/.lake

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

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

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

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

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

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

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

README.md

@@ -0,0 +1 @@
+# GaloisRamification