Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
Akwardbro committed Jul 7, 2024
2 parents 3718f7c + a84966a commit 9989bfd
Showing 18 changed files with 1,315 additions and 897 deletions.
6 changes: 6 additions & 0 deletions RamificationGroup/DecompositionGroup.lean
Original file line number Diff line number Diff line change
@@ -27,9 +27,15 @@ def decompositionGroup : Subgroup (S ≃ₐ[R] S) where
apply Valuation.IsEquiv_comap_symm
exact h

/-- This stupid theorem should be parametrized over `Subgroup (S ≃ₐ[R] S)`. -/
theorem decompositionGroup_one : (1 : decompositionGroup R S).1 = .refl := by
simp only [OneMemClass.coe_one, AlgEquiv.aut_one]

/-- This stupid theorem should be parametrized over `Subgroup (S ≃ₐ[R] S)`. -/
theorem refl_mem_decompositionGroup : .refl ∈ decompositionGroup R S := by
rw [← decompositionGroup_one R S]
exact (1 : decompositionGroup R S).2

section eq_top

variable {K L : Type*} [Field K] [Field L] [vK : Valued K ℤₘ₀] [IsDiscrete vK.v] [vL : Valued L ℤₘ₀] [Algebra K L] [FiniteDimensional K L]
38 changes: 26 additions & 12 deletions RamificationGroup/ForMathlib/Algebra/Algebra/PowerBasis.lean
Original file line number Diff line number Diff line change
@@ -1,14 +1,28 @@
import Mathlib.RingTheory.PowerBasis

namespace PowerBasis

variable {R S : Type*} [CommRing R] [Ring S] [Algebra R S]
{S' : Type*} [Semiring S'] [Algebra R S']

theorem algEquiv_ext (pb : PowerBasis R S) {f g : S ≃ₐ[R] S'} (h : f pb.gen = g pb.gen) :
f = g := by
ext x
rw [show f x = g x ↔ f.toAlgHom x = g.toAlgHom x by rfl]
revert x
rw [← AlgHom.ext_iff]
apply algHom_ext _ h
open Algebra PowerBasis Polynomial

variable {R A : Type*} [CommRing R] [Ring A] [Algebra R A]
{B : Type*} [Semiring B] [Algebra R B]
{F : Type*} [FunLike F A B] [AlgHomClass F R A B]

theorem Algebra.exists_eq_aeval_generator {s : A} (hgen : adjoin R {s} = ⊤) (x : A) :
∃ f : R[X], x = aeval s f := by
have hx : x ∈ (⊤ : Subalgebra R A) := trivial
rw [← hgen, adjoin_singleton_eq_range_aeval] at hx
rcases hx with ⟨p, hp⟩
exact ⟨p, hp.symm⟩

theorem Algebra.algHomClass_ext_generator {s : A} (hgen : adjoin R {s} = ⊤)
{f g : F} (h : f s = g s) :
f = g := by
apply DFunLike.ext
intro x
have hx : x ∈ (⊤ : Subalgebra R A) := trivial
rw [← hgen, adjoin_singleton_eq_range_aeval] at hx
rcases hx with ⟨p, hp⟩
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe] at hp
rw [← hp, ← Polynomial.aeval_algHom_apply, ← Polynomial.aeval_algHom_apply, h]

theorem PowerBasis.algHom_ext' (pb : PowerBasis R A) {f g : F} (h : f pb.gen = g pb.gen) :
f = g := Algebra.algHomClass_ext_generator (adjoin_gen_eq_top pb) h
12 changes: 8 additions & 4 deletions RamificationGroup/ForMathlib/DiscreteValuationRing/Basic.lean
Original file line number Diff line number Diff line change
@@ -13,8 +13,7 @@ variable {ϖ x : A} (hϖ : Irreducible ϖ)

theorem unit_mul_irreducible_of_irreducible (hx : Irreducible x) : ∃u : A, IsUnit u ∧ x = u * ϖ := by
obtain ⟨u, hu⟩ : ∃u : A, x = u * ϖ := by
refine exists_eq_mul_left_of_dvd (addVal_le_iff_dvd.mp ?_)
apply le_of_eq
refine exists_eq_mul_left_of_dvd <| addVal_le_iff_dvd.mp <| le_of_eq ?_
rw [addVal_uniformizer hx, addVal_uniformizer hϖ]
have : IsUnit u := Or.resolve_right (Irreducible.isUnit_or_isUnit hx hu) hϖ.not_unit
use u
@@ -39,12 +38,17 @@ theorem mul_irreducible_square_of_not_unit_of_not_irreducible (h1 : ¬Irreducibl
theorem irreducible_of_irreducible_add_addVal_ge_two (hx : Irreducible x) {y : A} : Irreducible (x + y * ϖ ^ 2) := by
rcases unit_mul_irreducible_of_irreducible hϖ hx with ⟨u, hu, hxu⟩
rw [hxu, pow_two, ← mul_assoc, ← add_mul]
apply (irreducible_isUnit_mul _).mpr hϖ
apply LocalRing.is_unit_of_unit_add_nonunit hu
apply (irreducible_isUnit_mul (LocalRing.is_unit_of_unit_add_nonunit hu _)).mpr hϖ
simp only [mem_nonunits_iff, IsUnit.mul_iff, not_and]
exact fun _ ↦ Irreducible.not_unit hϖ

theorem maximalIdeal_pow_eq_span_irreducible_pow (n : ℕ) : maximalIdeal A ^ n = Ideal.span {ϖ ^ n} := by
rw [Irreducible.maximalIdeal_eq hϖ, Ideal.span_singleton_pow]

end uniformiser

section ramiIdx

/- Show `p = P^e` under suitable conditions. -/

end ramiIdx
2 changes: 1 addition & 1 deletion RamificationGroup/ForMathlib/LocalRing/Basic.lean
Original file line number Diff line number Diff line change
@@ -9,7 +9,7 @@ noncomputable def ramificationIdx : ℕ := Ideal.ramificationIdx (algebraMap A B

noncomputable def inertiaDeg : ℕ := Ideal.inertiaDeg (algebraMap A B) (maximalIdeal A) (maximalIdeal B)

instance instAlgebraResidue : Algebra (ResidueField A) (ResidueField B) :=
instance : Algebra (ResidueField A) (ResidueField B) :=
Ideal.Quotient.algebraQuotientOfLEComap <| le_of_eq (((local_hom_TFAE <| algebraMap A B).out 0 4 rfl rfl).mp is_local).symm

variable {A B}
Loading

0 comments on commit 9989bfd

Please sign in to comment.