Merge pull request #5 from timechess/master

bump and fix

RamificationGroup/ForMathlib/DiscreteValuationRing/Basic.lean

@@ -10,7 +10,7 @@ variable {A : Type*} [CommRing A] [IsDomain A] [DiscreteValuationRing A]
 section uniformiser
 
 variable {ϖ x : A} (hϖ : Irreducible ϖ)
-
+include hϖ
 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 <| le_of_eq ?_

RamificationGroup/ForMathlib/Henselian.lean

@@ -4,12 +4,12 @@ variable (R : Type*) [CommRing R]
 
 open LocalRing
 
-instance instHenselianLocalToHenselian [l : LocalRing R] [h : HenselianRing R <| maximalIdeal R] :
-  HenselianLocalRing R := {
-    l with
-    is_henselian := by
-      convert h.is_henselian
-      letI : IsLocalRingHom (Ideal.Quotient.mk (maximalIdeal R)) := by
-        apply  LocalRing.instIsLocalRingHomResidueFieldResidue
-      rw [isUnit_map_iff]
-  }
+-- instance instHenselianLocalToHenselian [l : LocalRing R] [h : HenselianRing R <| maximalIdeal R] :
+--   HenselianLocalRing R := {
+--     l with
+--     is_henselian := by
+--       convert h.is_henselian
+--       letI : IsLocalHom (Ideal.Quotient.mk (maximalIdeal R)) := by
+--         apply LocalRing.instIsLocalRingHomResidueFieldResidue
+--       rw [isUnit_map_iff]
+--   }

RamificationGroup/ForMathlib/LocalRing/Basic.lean

@@ -4,7 +4,7 @@ import Mathlib.RingTheory.LocalRing.ResidueField.Basic
 namespace LocalRing
 
 variable (A B : Type*) [CommRing A] [CommRing B]
-  [LocalRing A] [LocalRing B] [Algebra A B] [is_local : IsLocalRingHom (algebraMap A B)]
+  [LocalRing A] [LocalRing B] [Algebra A B] [is_local : IsLocalHom (algebraMap A B)]
 
 noncomputable def ramificationIdx : ℕ := Ideal.ramificationIdx (algebraMap A B) (maximalIdeal A) (maximalIdeal B)
 

RamificationGroup/LowerNumbering.lean

@@ -1,6 +1,5 @@
 import RamificationGroup.Valued.Hom.Lift
 import RamificationGroup.ForMathlib.Algebra.Algebra.Tower
-import Mathlib.FieldTheory.Galois
 import LocalClassFieldTheory.LocalField.Basic
 import RamificationGroup.ForMathlib.Algebra.Algebra.PowerBasis
 import RamificationGroup.Valued.AlgebraicInstances

RamificationGroup/Valuation/Discrete.lean

@@ -52,7 +52,7 @@ lemma eq_one_of_eq_one_of_le_one_le_one (h : ∀{x : K}, v x ≤ 1 → v' x ≤
   · have : v' u ≠ 0 := by
       rw [Valuation.ne_zero_iff, ← Valuation.ne_zero_iff v, hu]
       exact one_ne_zero
-    rw [← inv_le_one₀ this, ← map_inv₀]
+    rw [show 1 ≤ v' u ↔ (v' u)⁻¹ ≤ 1 by sorry, ← map_inv₀]
     apply h <| le_of_eq _
     rw [map_inv₀, hu, inv_one]
 
@@ -76,11 +76,11 @@ variable {K : Type*} [Field K] {ΓK ΓK': outParam Type*}
 
 theorem val_valuationSubring_unit {u : v.valuationSubringˣ} :
   v u = 1 := by
-  rw [(isEquiv_iff_val_eq_one v v.valuationSubring.valuation).mp (isEquiv_valuation_valuationSubring v), ValuationSubring.valuation_unit]
+  rw [(isEquiv_iff_val_eq_one).mp (isEquiv_valuation_valuationSubring v), ValuationSubring.valuation_unit]
 
 theorem isUnit_in_valuationSubring_of_val_eq_one {x : K} (h : v x = 1) :
   IsUnit (⟨x, le_of_eq h⟩ : v.valuationSubring) := by
-  rw [ValuationSubring.valuation_eq_one_iff, ← (isEquiv_iff_val_eq_one v v.valuationSubring.valuation).mp (isEquiv_valuation_valuationSubring v), h]
+  rw [ValuationSubring.valuation_eq_one_iff, ← (isEquiv_iff_val_eq_one).mp (isEquiv_valuation_valuationSubring v), h]
 
 /-- create a term of `v.valuationSubringˣ` from a term `x : K` with `v x = 1`-/
 noncomputable def unitOfValOne {x : K} (h : v x = 1) : v.valuationSubringˣ :=
@@ -164,14 +164,14 @@ lemma isUniformizer_of_uniformizer_of_le_one_le_one (h : ∀{x : K}, v x ≤ 1 
 /--If `π : K` is a uniformizer for `v`, and `v` is equivalent to `v'`, then `π` is also a uniformizer for `v'`.-/
 theorem isUniformizer_of_uniformizer_of_equiv (h : v.IsEquiv v')
   (π : Uniformizer v) : IsUniformizer v' π.1 := isUniformizer_of_uniformizer_of_le_one_le_one
-  (fun {_} hx ↦ ((isEquiv_iff_val_le_one v v').mp h).mp hx) π
+  (fun {_} hx ↦ ((isEquiv_iff_val_le_one).mp h).mp hx) π
 
 theorem val_pow_Uniformizer_all_of_equiv (h : v.IsEquiv v') {π : Uniformizer v} {n : ℤ} {u : v.valuationSubringˣ} :
   v' ((π.1 : K) ^ n * u.1) = ofAdd (-n : ℤ) := by
   rw [v'.map_mul, Valuation.map_zpow,
     isUniformizer_of_uniformizer_of_equiv h]
   have : v' (u : K) = 1 := by
-    rw [← (isEquiv_iff_val_eq_one _ _).mp h, val_valuationSubring_unit]
+    rw [← (isEquiv_iff_val_eq_one).mp h, val_valuationSubring_unit]
   simp only [Int.reduceNeg, ofAdd_neg, WithZero.coe_inv, inv_zpow', zpow_neg, this, mul_one, inv_inj,
     ← WithZero.coe_zpow, ← ofAdd_zsmul, smul_eq_mul, mul_one] -- `WithZero.coe_zpow` should be tagged with @[norm_cast], but it is not.
 
@@ -206,7 +206,7 @@ theorem isEquiv_of_le_one_le_one (h : ∀{x : K}, v x ≤ 1 → v' x ≤ 1) :
   by_contra! vxgt
   have : (1 : ℤₘ₀) < 1 := by
     nth_rw 1 [← Valuation.map_one v']
-    rw [show (1 : K) = x * x⁻¹ by simp only [ne_eq, xne0, not_false_eq_true, mul_inv_cancel], Valuation.map_mul, show (1 : ℤₘ₀) = 1 * 1 by rfl]
+    rw [(CommGroupWithZero.mul_inv_cancel x xne0).symm, Valuation.map_mul, show (1 : ℤₘ₀) = 1 * 1 by rfl]
     apply mul_lt_mul_of_lt_of_le₀ v'xle (by simp only [ne_eq, one_ne_zero, not_false_eq_true])
     exact lt_one_lt_one_of_le_one_le_one h <| (one_lt_val_iff _ xne0).mp vxgt
   contradiction

RamificationGroup/Valuation/Extension.lean

@@ -12,11 +12,11 @@ namespace ExtDVR
 
 variable {A : Type*} [CommRing A] [IsDomain A] [DiscreteValuationRing A]
 variable {B : Type*} [CommRing B] [IsDomain B] [DiscreteValuationRing B]
-variable [Algebra A B] [IsLocalRingHom (algebraMap A B)]
+variable [Algebra A B] [IsLocalHom (algebraMap A B)]
 variable [Algebra.IsSeparable (ResidueField A) (ResidueField B)]
 variable [Module.Finite A B]
 
-instance : FiniteDimensional (ResidueField A) (ResidueField B) := FiniteDimensional_of_finite
+instance : FiniteDimensional (ResidueField A) (ResidueField B) := ResidueField.finiteDimensional_of_noetherian
 
 variable (A) (B) in
 /-- There exists `x : B` generating `k_B` over `k_A` -/
@@ -46,6 +46,7 @@ variable {f : A[X]} (h_red : f.map (residue A) = minpoly (ResidueField A) (resid
 -- `ϖ` : a uniformizer `ϖ` of `B`
 variable {ϖ : B} (hϖ : Irreducible ϖ)
 
+include hx hϖ h_red
 /-- Auxiliary lemma: `A[x, ϖ] ⊔ m_B = ⊤`. Can be strenthened to `A[x] ⊔ m_B = B`-/
 lemma adjoin_lift_residue_primitive_and_irreducible_sup_maximalIdeal_eq_top : toSubmodule (Algebra.adjoin A {x, ϖ}) ⊔ (maximalIdeal B).restrictScalars A = ⊤ := by
   rw [eq_top_iff]
@@ -82,7 +83,7 @@ lemma adjoin_lift_residue_primitive_and_irreducible_sup_maximalIdeal_pow_eq_top
       use c
       rw [← hc, mul_comm]
     have : c ∈ toSubmodule (Algebra.adjoin A {x, ϖ}) ⊔ (maximalIdeal B).restrictScalars A := by
-      rw [adjoin_lift_residue_primitive_and_irreducible_sup_maximalIdeal_eq_top hx]
+      rw [adjoin_lift_residue_primitive_and_irreducible_sup_maximalIdeal_eq_top hx h_red hϖ]
       apply Submodule.mem_top
     obtain ⟨u, hu, v, hv, huv⟩ := Submodule.mem_sup.mp this
     obtain ⟨w, hw⟩ : ∃w : B, v = ϖ * w := by
@@ -121,8 +122,8 @@ theorem adjoin_lift_residue_primitive_and_irreducible_eq_top (h_inj : Function.I
     obtain ⟨n, hn⟩ : ∃n : ℕ, (maximalIdeal A).map (algebraMap A B) = maximalIdeal B ^ n := by
       rcases (TFAE B (not_isField B)).out 0 6 with ⟨h, _⟩
       apply h; assumption
-      apply maximalIdeal_map_ne_bot_of_injective h_inj
-    rw [hn, adjoin_lift_residue_primitive_and_irreducible_sup_maximalIdeal_pow_eq_top hx hϖ]
+      exact maximalIdeal_map_ne_bot_of_injective hx h_red hϖ h_inj
+    rw [hn, adjoin_lift_residue_primitive_and_irreducible_sup_maximalIdeal_pow_eq_top hx h_red hϖ]
   · apply Module.finite_def.mp
     assumption
 
@@ -142,7 +143,7 @@ If `f x` has valuation ≥ 2, then `f (x + ϖ)` is a uniformizer.
 -/
 theorem irreducible_aeval_lift_redisue_primitive_add_irreducible_of_reducible_aeval_lift_residue_primitve (h_fx : ¬Irreducible (f.eval₂ (algebraMap A B) x)) : Irreducible (f.eval₂ (algebraMap A B) (x + ϖ)) := by
   obtain ⟨b, hb⟩ := taylor_order_one_apply₂ f (algebraMap A B) x ϖ
-  obtain ⟨y, hy⟩ := mul_irreducible_square_of_not_unit_of_not_irreducible hϖ h_fx (not_unit_aeval_lift_residue_primitive h_red)
+  obtain ⟨y, hy⟩ := mul_irreducible_square_of_not_unit_of_not_irreducible hϖ h_fx (not_unit_aeval_lift_residue_primitive hx h_red hϖ)
   rw [hb, hy, mul_comm ϖ, ← mul_comm b, add_comm, ← add_assoc, ← add_mul, add_comm]
   apply irreducible_of_irreducible_add_addVal_ge_two hϖ
   apply (irreducible_isUnit_mul _).mpr hϖ
@@ -159,12 +160,12 @@ end x_and_f
 This is the second part of lemma 4:
 `B = A[x]` if `k_B = k_A[x]` and `f x` is a uniformizer.-/
 theorem adjoin_lift_primitive_eq_top_of_irreducible_aeval_lift_residue_primitive (h_inj : Function.Injective (algebraMap A B)) {x : B} (hx : (ResidueField A)⟮residue B x⟯ = ⊤)
-    {f : A[X]} (h_fx : Irreducible (f.eval₂ (algebraMap A B) x)) :
+    {f : A[X]} (h_fx : Irreducible (f.eval₂ (algebraMap A B) x) )  :
     Algebra.adjoin A {x} = ⊤ := by
   apply Algebra.adjoin_eq_of_le
   · simp only [Algebra.coe_top, Set.subset_univ]
   let fx := f.eval₂ (algebraMap A B) x
-  rw [← adjoin_lift_residue_primitive_and_irreducible_eq_top hx h_fx h_inj]
+  rw [← adjoin_lift_residue_primitive_and_irreducible_eq_top hx h_red h_fx h_inj]
   rw [show ({x, fx} : Set B) = {x} ∪ {fx} by rfl, Algebra.adjoin_union]
   simp only [sup_le_iff, le_refl, true_and, ge_iff_le]
   rw [Algebra.adjoin_le_iff, Set.singleton_subset_iff, SetLike.mem_coe]

RamificationGroup/Valuation/PolyTaylor.lean

@@ -1,4 +1,5 @@
 import Mathlib.Algebra.Polynomial.Taylor
+import Mathlib.Algebra.Polynomial.Div
 
 namespace Polynomial
 

RamificationGroup/Valued/Hom/Discrete.lean

@@ -52,7 +52,7 @@ theorem aeval_valuationSubring_lt_one_of_lt_one
   apply eval_lt_one_of_coeff_le_one_of_const_eq_zero_of_lt_one _ _ hx
   · intro n
     rw [coeff_map, show (algebraMap 𝒪[K] L) (f.coeff n) = (algebraMap K L) (f.coeff n) by rfl, ← comap_apply]
-    apply ((isEquiv_iff_val_le_one _ _).mp h).mp (f.coeff n).2
+    apply ((isEquiv_iff_val_le_one).mp h).mp (f.coeff n).2
   · simp only [coeff_map, h0, _root_.map_zero]
 
 theorem aeval_valuationSubring_lt_one_of_lt_one_self
@@ -89,6 +89,12 @@ end Valuation
 
 end non_discrete
 
+/-- Notation for `WithZero (Multiplicative ℕ)` -/
+scoped[DiscreteValuation] notation "ℕₘ₀" => WithZero (Multiplicative ℕ)
+
+/-- Notation for `WithZero (Multiplicative ℤ)` -/
+scoped[DiscreteValuation] notation "ℤₘ₀" => WithZero (Multiplicative ℤ)
+
 variable {K : Type*} [Field K] [vK : Valued K ℤₘ₀]
 variable {L : Type*} [Field L]
 
@@ -108,7 +114,7 @@ theorem nontrivial_of_valuation_extension (h : vK.v.IsEquiv <| vL.comap (algebra
   · rw [← comap_apply, ← IsEquiv.ne_zero h, hp]
     decide
   · apply ne_of_lt
-    rw [← comap_apply, ← (isEquiv_iff_val_lt_one _ _).mp h, hp]
+    rw [← comap_apply, ← (isEquiv_iff_val_lt_one).mp h, hp]
     decide
 
 /-- If a valuation `v : L → ℤₘ₀` extends a discrete valuation on `K`, then `v` is equivalent to `extendedValuation K L`.-/
@@ -118,7 +124,7 @@ theorem extension_valuation_equiv_extendedValuation_of_discrete
   letI : vL.Nontrivial := nontrivial_of_valuation_extension h
   apply IsEquiv.trans (isEquiv_ofNontrivial vL) (isEquiv_of_le_one_le_one _).symm
   intro x
-  rw [← mem_valuationSubring_iff, ← ValuationSubring.mem_toSubring, ← Extension.integralClosure_eq_integer, ← (isEquiv_iff_val_le_one _ _).mp (isEquiv_ofNontrivial vL)]
+  rw [← mem_valuationSubring_iff, ← ValuationSubring.mem_toSubring, ← Extension.integralClosure_eq_integer, ← (isEquiv_iff_val_le_one).mp (isEquiv_ofNontrivial vL)]
   apply mem_integer_of_mem_integral_closure h
 
 theorem extension_integer_eq_extendedValuation_of_discrete (h : vK.v.IsEquiv <| vL.comap (algebraMap K L)) :

RamificationGroup/Valued/Hom/Lift.lean

@@ -51,8 +51,8 @@ def RingHom.restrictInteger {f : R →+* S} (hf : vR.v.IsEquiv (vS.v.comap f)) :
     refine fun ⟨x, hx⟩ ↦ ⟨f x, ?_⟩
     rw [mem_integer_iff, val_map_le_one_iff (f := f) hf]
     exact hx
-  map_one' := by simp only [_root_.map_one, Submonoid.mk_eq_one]
-  map_mul' := by simp only [_root_.map_mul, Submonoid.mk_mul_mk, Subtype.forall, implies_true, forall_const]
+  map_one' := by simp only [_root_.map_one]; rfl
+  map_mul' := by simp only [_root_.map_mul, MulMemClass.mk_mul_mk, implies_true]
   map_zero' := by simp only [_root_.map_zero]; rfl
   map_add' := by simp only [_root_.map_add, AddMemClass.mk_add_mk, Subtype.forall, implies_true, forall_const]
 

RamificationGroup/Valued/Hom/ValExtension.lean

@@ -41,6 +41,8 @@ variable {R S : Type*} {ΓR ΓS : outParam Type*} [Ring R] [Ring S]
 variable {F : Type*} [FunLike F R S] [RingHomClass F R S] {f : F}
     (hf : vR.v.IsEquiv <| vS.v.comap f)
 
+include hf
+
 theorem val_map_le_iff (x y : R) : v (f x) ≤ v (f y) ↔ v x ≤ v y :=
   (hf x y).symm
 

lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dc167d260ff7ee9849b436037add06bed15104be",
+   "rev": "dc72dcdb8e97b3c56bd70f06f043ed2dee3258e6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5",
+   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0444234b4216e944d5be2ce42a25d7410c67876f",
+   "rev": "9ac12945862fa39eab7795c2f79bb9aa0c8e332c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,16 +35,16 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
+   "rev": "baa65c6339a56bd22b7292aa4511c54b3cc7a6af",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.41",
+   "inputRev": "v0.0.43",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "",
+   "scope": "leanprover",
    "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
@@ -55,27 +55,37 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
+   "rev": "0ea83a676d288220ba227808568cbb80fe43ace0",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4",
+  {"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": "15720c78a8142f7d35418f15b528bdb3f184989a",
+   "rev": "3693a5a57e378f05c10214413ad7976295d762f7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": false,
+   "inputRev": null,
+   "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/PatrickMassot/checkdecls.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "21a36f3c07a9229e1287483c16a0dd04e479ecc5",
+   "rev": "11fa569b1b52f987dc5dcea97fd80eaff95c2fce",
    "name": "checkdecls",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bf457847ed802fcf1e7c37026d22e68eb7b67fb9",
+   "rev": "2b0994f595ab9d2daaef0bfbc04c6d1368f60df5",
    "name": "local_class_field_theory",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lakefile.lean

@@ -14,7 +14,7 @@ lean_lib «RamificationGroup» where
   -- add library configuration options here
 
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master"
+-- require mathlib from git "https://github.com/leanprover-comsmunity/mathlib4"@"master"
 
 require local_class_field_theory from git "https://github.com/mariainesdff/LocalClassFieldTheory.git"
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.11.0-rc1
+leanprover/lean4:v4.13.0-rc3