Skip to content

Commit

Permalink
continuous
Browse files Browse the repository at this point in the history
Akwardbro committed Aug 31, 2024
1 parent 283bf13 commit 04d5501
Showing 4 changed files with 692 additions and 211 deletions.
63 changes: 63 additions & 0 deletions RamificationGroup/Herbramd_bij.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
import RamificationGroup.Herbrand_aux
import Mathlib.RingTheory.Valuation.Basic

open scoped Classical
open HerbrandFunction DiscreteValuation AlgEquiv Valued
open DiscreteValuation Subgroup Set Function Finset BigOperators Int Valued

variable (K L : Type*) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [vK : Valued K ℤₘ₀] [Valuation.IsDiscrete vK.v] [vL : Valued L ℤₘ₀] [Algebra K L] [IsValExtension K L] [FiniteDimensional K L] [CompleteSpace K] [Algebra.IsSeparable K L]
[Algebra.IsSeparable (LocalRing.ResidueField ↥𝒪[K]) (LocalRing.ResidueField ↥𝒪[L])]

variable (R S : Type*) {ΓR : outParam Type*} [CommRing R] [Ring S] [LinearOrderedCommGroupWithZero ΓR] [vR : Valued R ΓR] [vS : Valued S ℤₘ₀] [Algebra R S]


theorem phi_linear_section_aux {n : ℤ} {x : ℚ} (hx : n ≤ x ∧ x < n + 1) {gen : 𝒪[L]} (hgen : Algebra.adjoin 𝒪[K] {gen} = ⊤) : phi K L x = phi K L n + (phi K L (n + 1) - phi K L n) * (x - n) := by
by_cases hc : 0 < x
· have hn : (0 : ℚ) ≤ n := by sorry
by_cases hc' : (0 : ℚ) < n
· rw [phi_eq_sum_card K L hc]
nth_rw 1 [phi_eq_sum_card K L hc']
sorry
· have hn' : n = 0 := by sorry
simp only [hn', cast_zero, zero_add, sub_zero]
sorry
· push_neg at hc
rw [phi_eq_self_of_le_zero K L hc]
sorry

theorem phi_Bijective_section_aux {n : ℤ} {gen : 𝒪[L]} (hgen : Algebra.adjoin 𝒪[K] {gen} = ⊤) : ∀ (y : ℚ) , (phi K L n) ≤ y ∧ y < (phi K L (n + 1)) → ∃ (x : ℚ), phi K L x = y := by
intro y ⟨hy1, hy2⟩
use (n + ((y - phi K L n) / (phi K L (n + 1) - phi K L n)))
have hx : n ≤ (n + ((y - phi K L n) / (phi K L (n + 1) - phi K L n))) ∧ (n + ((y - phi K L n) / (phi K L (n + 1) - phi K L n))) < n + 1 := by sorry
rw [phi_linear_section_aux K L hx hgen]
rw [add_comm (n : ℚ) ((y - phi K L n) / (phi K L (n + 1) - phi K L n)), add_sub_assoc, sub_self, add_zero, ]
have : (phi K L (↑n + 1) - phi K L ↑n) * ((y - phi K L ↑n) / (phi K L (↑n + 1) - phi K L ↑n)) = (y - phi K L y) := by sorry
rw [this]

theorem phi_infty (y : ℚ) : ∃ n : ℤ, phi R S n ≤ y ∧ y < phi R S (n + 1) := by
by_contra hc
push_neg at hc
have hz : ∀ n : ℤ, phi R S n ≤ y := by
intro n
sorry
have hq : ∀ n : ℚ, phi R S n ≤ y := by
intro n
apply le_trans (b := phi R S ⌈n⌉)
· by_cases hc : n = ⌈n⌉
· rw [← hc]
· apply le_of_lt; apply phi_strictMono R S _
apply lt_of_le_of_ne; apply Int.le_ceil; exact hc
· apply hz ⌈n⌉
sorry

theorem phi_Bijective_aux : Function.Bijective (phi R S) := by
constructor
· rintro a1 a2 h
contrapose! h
by_cases h1 : a1 > a2
· apply ne_of_gt (phi_strictMono R S h1)
· push_neg at *
apply ne_of_lt (phi_strictMono R S (lt_of_le_of_ne h1 h))
· rintro y
obtain ⟨n, hn⟩ := phi_infty R S y
apply phi_Bijective_section_aux R S (n := n) y hn
473 changes: 265 additions & 208 deletions RamificationGroup/HerbrandFunction.lean
Original file line number Diff line number Diff line change
@@ -18,18 +18,29 @@ namespace HerbrandFunction

variable (R S : Type*) {ΓR : outParam Type*} [CommRing R] [Ring S] [LinearOrderedCommGroupWithZero ΓR] [vR : Valued R ΓR] [vS : Valued S ℤₘ₀] [Algebra R S]

theorem Ramification_Group_card_pos {u : ℚ} : 0 < Nat.card G(S/R)_[⌈u⌉] := by
haveI : Finite G(S/R)_[⌈u⌉] := sorry
refine Nat.card_pos

-- by definition of relindex, it's always 1 when u < 0
noncomputable def phiDeriv (u : ℚ) : ℚ :=
1 / (relindex G(S/R)_[(⌈u⌉)] G(S/R)_[0])
--(Nat.card G(S/R)_[(⌈u⌉)] : ℚ) / (Nat.card G(S/R)_[0] : ℚ)
--1 / Nat.card (G(S/R)_[0] ⧸ ((G(S/R)_[⌈u⌉]).subgroupOf G(S/R)_[0]))
--1 / (relindex G(S/R)_[(⌈u⌉)] G(S/R)_[0])
(Nat.card G(S/R)_[(max 0 ⌈u⌉)] : ℚ) / (Nat.card G(S/R)_[0] : ℚ)

noncomputable def phi (u : ℚ) : ℚ :=
∑ x in Finset.Icc 1 (⌈u⌉ - 1), (phiDeriv R S x) + (u - (max 0 (⌈u⌉ - 1))) * (phiDeriv R S u)

theorem phiDeriv_eq_one_of_le_zero {u : ℚ} (hu : u ≤ 0) : phiDeriv R S u = 1 := by
unfold phiDeriv relindex
simp
apply lowerRamificationGroup.antitone
apply ceil_nonpos hu
unfold phiDeriv
have hu' : ⌈u⌉ ≤ 0 := by exact ceil_nonpos hu
simp only [hu', max_eq_left]
apply div_self
--card of ramigroup ne one
apply ne_of_gt
simp only [Nat.cast_pos]
apply Ramification_Group_card_pos R S (u := 0)

theorem phi_eq_self_of_le_zero {u : ℚ} (hu : u ≤ 0) : phi R S u = u := by
unfold phi
@@ -41,11 +52,20 @@ theorem phi_eq_self_of_le_zero {u : ℚ} (hu : u ≤ 0) : phi R S u = u := by
_ = u := by simp [h]

theorem phiDeriv_pos (u : ℚ) : 0 < phiDeriv R S u := by
unfold phiDeriv relindex index
apply one_div_pos.2
have h : 0 < (Nat.card (↥ G(S/R)_[0] ⧸ subgroupOf G(S/R)_[⌈u⌉] G(S/R)_[0])) := by
apply Nat.card_pos_iff.2sorry, sorry
exact_mod_cast h
unfold phiDeriv
apply div_pos
<;> simp only [Nat.cast_pos]
have : max 0 ⌈u⌉ = ⌈max 0 (⌈u⌉ : ℚ)⌉ := by
symm
apply Int.ceil_eq_iff.2
constructor
· apply lt_of_lt_of_le (b := ↑(max 0 ⌈u⌉))
linarith
simp only [cast_max, cast_zero, le_refl]
· simp only [cast_max, cast_zero, le_refl]
rw [this]
apply Ramification_Group_card_pos R S (u := max 0 ⌈u⌉)
apply Ramification_Group_card_pos R S (u := 0)

theorem phiDeriv_eq_ceil {u : ℚ} : phiDeriv R S u = phiDeriv R S ⌈u⌉ := by
unfold phiDeriv
@@ -90,25 +110,129 @@ theorem phi_of_pos_of_le_one {u : ℚ} (h1 : 0 < u) (h2 : u ≤ 1) : phi R S u =

#check Finset.sum_range_sub_sum_range

theorem Finset.sum_Icc_sub_sum_Icc {n : ℤ} {m : ℤ} (hnm : n ≤ m) : ∑ x in Finset.Icc 1 m, phiDeriv R S x - ∑ x in Finset.Icc 1 n, phiDeriv R S x = ∑ x in Finset.Icc (n + 1) m, phiDeriv R S x := by sorry
theorem Finset.sum_Icc_sub_sum_Icc {n : ℤ} {m : ℤ} (hn : 1 ≤ n) (hnm : n ≤ m) : ∑ x in Finset.Icc 1 m, phiDeriv R S x - ∑ x in Finset.Icc 1 n, phiDeriv R S x = ∑ x in Finset.Icc (n + 1) m, phiDeriv R S x := by
have hd : Disjoint (Finset.Icc 1 n) (Finset.Icc (n + 1) m) := by
refine Disjoint.symm ((fun {α} {s t} ↦ Finset.disjoint_left.mpr) ?_)
intro a ha
rw [Finset.mem_Icc] at *
apply not_and_or.2
right
linarith [ha.1]
have hu : Finset.Icc 1 m = Finset.Icc 1 n ∪ Finset.Icc (n + 1) m := by
ext x
rw [Finset.mem_union]
repeat rw [Finset.mem_Icc]
constructor <;> intro h
· by_cases hc : x ≤ n
· left
exact ⟨h.1, hc⟩
· right
exact ⟨by linarith [hc], h.2
· constructor
· match h with
| Or.inl h => exact h.left
| Or.inr h => linarith [hn, h.right]
· match h with
| Or.inl h => linarith [h.left]
| Or.inr h => exact h.right
rw [sub_eq_iff_eq_add', hu]
apply Finset.sum_union hd

theorem insert_Icc_left (a b : ℤ) (ha : a ≤ b): Finset.Icc a b = insert a (Finset.Icc (a + 1) b) := by
ext x
constructor
· intro h
obtain ⟨h1, h2⟩ := Finset.mem_Icc.1 h
rw [Finset.insert_eq]
apply Finset.mem_union.2
by_cases h : x = a
· left
simp [h]
· right
push_neg at *
apply Finset.mem_Icc.2
constructor
· apply Int.le_of_sub_one_lt
simp [lt_of_le_of_ne h1 h.symm]
exact h2
· rw [Finset.insert_eq, Finset.mem_union, Finset.mem_Icc, Finset.mem_Icc]
rintro h
rcases h with h | ⟨h1, h2⟩
· constructor
· apply le_of_eq (Finset.mem_singleton.1 h).symm
· apply le_trans (le_of_eq (Finset.mem_singleton.1 h)) ha
· constructor
· linarith [h1]
· exact h2

theorem phi_strictMono_of_gt_one {a b : ℚ} (hb : 1 < b) (hab : a < b) : phi R S a < phi R S b := by
theorem insert_Icc_right (a b : ℤ) (h : a ≤ b) : Finset.Icc a b = insert b (Finset.Icc a (b - 1)) := by
apply Finset.Subset.antisymm
· intro x hx
rw [Finset.insert_eq b (Finset.Icc a (b - 1))]
apply Finset.mem_union.2
by_cases h : x = b
· left
simp [h]
· right
simp at hx
simp
constructor
· exact hx.1
· apply Int.le_of_sub_one_lt
apply lt_of_le_of_ne
linarith
push_neg at h
simp [h]
· rw [Finset.insert_eq b (Finset.Icc a (b - 1))]
apply Finset.union_subset
simp [h]
apply Finset.Icc_subset_Icc
rfl; linarith

theorem sum_insert_left_aux (a b : ℤ) (ha : a ≤ b) (f : ℤ → ℕ) : (∑ x in Finset.Icc a b, f x) - f a = (∑ x in Finset.Icc (a + 1) b, f x):= by
calc
_ = ∑ x in insert a (Finset.Icc (a + 1) b), f x - f a := by
rw [insert_Icc_left _ _ ha]
_ = (∑ x in Finset.Icc (a + 1) b, f x) := by simp

theorem sum_insert_left_aux' (a b : ℤ) (h : a ≤ b) (f : ℤ → ℤ) : (∑ x in Finset.Icc a b, f x) - f a = (∑ x in Finset.Icc (a + 1) b, f x) := by
calc
_ = ∑ x in insert a (Finset.Icc (a + 1) b), f x - f a := by
rw [insert_Icc_left _ _ h]
_ = (∑ x in Finset.Icc (a + 1) b, f x) := by simp

theorem sum_insert_right_aux (a b : ℤ) (h : a ≤ b) (f : ℚ → ℚ) : (∑ x in Finset.Icc a b, f x) - f b = (∑ x in Finset.Icc a (b - 1), f x) := by sorry


theorem phi_strictMono_of_gt_one {a b : ℚ} (ha : 0 < a) (hb : 1 < b) (hab : a < b) : phi R S a < phi R S b := by
unfold phi
by_cases hceil : ⌈a⌉ = ⌈b⌉
· simp [phiDeriv_eq_ceil, hceil]
· simp only [hceil, phiDeriv_eq_ceil, ceil_intCast, cast_max, cast_zero, cast_sub, cast_one,
add_lt_add_iff_left]
apply (mul_lt_mul_right (by apply phiDeriv_pos R S)).2
simp [hab]
simp only [sub_lt_sub_iff_right, hab]
· calc
_ ≤ ∑ x in Finset.Icc 1 ⌈a⌉, phiDeriv R S x := by
apply le_trans (b := ∑x in Finset.Icc 1 (⌈a⌉ - 1), phiDeriv R S ↑x + 1 * phiDeriv R S ⌈a⌉)
rw [phiDeriv_eq_ceil R S]
apply add_le_add_left
apply (mul_le_mul_right (by apply phiDeriv_pos R S)).2
have : a - 1 ≤ (max 0 (⌈a⌉ - 1)) := by
simp
simp only [cast_max, cast_zero, cast_sub, cast_one, le_max_iff, tsub_le_iff_right,
zero_add, sub_add_cancel]
right; apply le_ceil
linarith [this]
have h : ∑ x in Finset.Icc 1 (⌈a⌉ - 1), phiDeriv R S ↑x + 1 * phiDeriv R S ↑⌈a⌉ = ∑ x in Finset.Icc 1 ⌈a⌉, phiDeriv R S ↑x := by sorry -- i have done this later
have h : ∑ x in Finset.Icc 1 (⌈a⌉ - 1), phiDeriv R S x + 1 * phiDeriv R S ⌈a⌉ = ∑ x in Finset.Icc 1 ⌈a⌉, phiDeriv R S x := by
have h' : ∑ x in Finset.Icc 1 ⌈a⌉, phiDeriv R S x - 1 * phiDeriv R S ⌈a⌉ = ∑ x in Finset.Icc 1 (⌈a⌉ - 1), phiDeriv R S x := by
by_cases hc : 1 ≤ a
· rw [one_mul]
apply sum_insert_right_aux 1 ⌈a⌉ ?_ (phiDeriv R S); exact one_le_ceil_iff.mpr ha
· have h : ⌈a⌉ = 1 := by
refine ceil_eq_on_Ioc 1 a ?_
simp only [cast_one, sub_self, Set.mem_Ioc, ha, true_and]
apply le_of_lt; push_neg at hc; exact hc
rw [h]; simp only [Finset.Icc_self, sum_singleton, cast_one, one_mul, sub_self, zero_lt_one, Finset.Icc_eq_empty_of_lt, sum_empty]
exact add_eq_of_eq_sub (id (Eq.symm h'))
apply le_of_eq h
_ ≤ ∑ x in Finset.Icc 1 (⌈b⌉ - 1), phiDeriv R S x := by
have h : ⌈a⌉ ≤ ⌈b⌉ - 1 := by
@@ -120,13 +244,15 @@ theorem phi_strictMono_of_gt_one {a b : ℚ} (hb : 1 < b) (hab : a < b) : phi R
exact hceil
apply le_sub_one_of_lt hc
have h' : Finset.Icc 1 (⌈a⌉) ⊆ Finset.Icc 1 (⌈b⌉ - 1) := by apply Finset.Icc_subset_Icc (by linarith) h
sorry
--apply sum_le_sum_of_subset h' --(f := phiDeriv R S)
apply Finset.sum_le_sum_of_subset_of_nonneg h'
intro i _ _
apply le_of_lt
apply phiDeriv_pos
_ < phi R S b := by
unfold phi
simp
simp only [cast_max, cast_zero, cast_sub, cast_one, lt_add_iff_pos_right]
apply mul_pos
simp
simp only [sub_pos, max_lt_iff]
constructor
· linarith [hb]
· linarith [ceil_lt_add_one b]
@@ -146,34 +272,22 @@ theorem phi_strictMono : StrictMono (phi R S) := by
push_neg at *
have hac : ⌈a⌉ = 1 := by
apply ceil_eq_iff.2
simp [ha0, ha1]
simp only [cast_one, sub_self, ha0, ha1, and_self]
· by_cases hb1 : b ≤ 1
· push_neg at *
have hbc : ⌈b⌉ = 1 := by
apply ceil_eq_iff.2
simp [lt_trans ha0 h, hb1]
simp only [cast_one, sub_self, lt_trans ha0 h, hb1, and_self]
have hceil : ⌈a⌉ = ⌈b⌉ := by simp [hac, hbc]
have hderiv : phiDeriv R S a = phiDeriv R S b := by
unfold phiDeriv
simp [hceil]
simp only [hceil, one_div]
rw [phi_of_pos_of_le_one R S ha0 ha1, phi_of_pos_of_le_one R S (by linarith) hb1]
simp [hderiv]
simp only [hderiv, gt_iff_lt]
apply (mul_lt_mul_right (by apply phiDeriv_pos R S)).2 h
· apply phi_strictMono_of_gt_one R S (by linarith) h
apply phi_strictMono_of_gt_one R S (by linarith) h

· apply phi_strictMono_of_gt_one R S (by linarith) (by linarith) h
apply phi_strictMono_of_gt_one R S (by linarith) (by linarith) h

theorem phi_inf (y : ℚ) : ∃ (n : ℕ) , ¬ phi R S n ≤ y := by sorry

--i don't know
--this proof is not good
theorem exist_aux (y : ℚ) : ∃ (n : ℕ) , phi R S (n - 1) ≤ y ∧ y < phi R S n := by
by_contra h
push_neg at h
obtain ⟨n, hn⟩ := phi_inf R S y
apply hn
apply h
sorry

theorem phi_Bijective : Function.Bijective (phi R S) := by
constructor
@@ -184,9 +298,6 @@ theorem phi_Bijective : Function.Bijective (phi R S) := by
· push_neg at *
apply ne_of_lt (phi_strictMono R S (lt_of_le_of_ne h1 h))
· rintro y
obtain ⟨n, ⟨hn, hn'⟩⟩ := exist_aux R S y
use (y - phi R S (n - 1)) * (relindex G(S/R)_[n] G(S/R)_[0]) + n - 1
unfold phi
sorry


@@ -226,6 +337,14 @@ theorem leftInverse_phi_psi : Function.LeftInverse (phi R S) (psi R S) := by
theorem phi_psi_eq_self (u : ℚ) : (phi R S) ((psi R S) u) = u := leftInverse_phi_psi R S u


@[simp]
theorem psi_phi_eq_self (u : ℚ) : (psi R S) ((phi R S) u) = u := by
rw [← Function.comp_apply (f := psi R S) (g := phi R S)]
unfold psi
rw [Function.invFun_comp (f := (phi R S))]
rfl; apply (phi_Bijective R S).injective


theorem psi_eq_self_of_le_neg_one {v : ℚ} (hv : v ≤ 0) : psi R S v = v := by
have h1 : phi R S (psi R S v) = v := by apply phi_psi_eq_self
have h2 : phi R S v = v := by apply phi_eq_self_of_le_zero R S hv
@@ -236,7 +355,7 @@ theorem psi_eq_self_of_le_neg_one {v : ℚ} (hv : v ≤ 0) : psi R S v = v := by
open scoped Classical


variable (K L : Type*) {ΓK : outParam Type*} [Field K] [Field L] [LinearOrderedCommGroupWithZero ΓK] [vK : Valued K ΓK] [vS : Valued L ℤₘ₀] [Algebra K L] [FiniteDimensional K L]
variable (K L : Type*) {ΓK : outParam Type*} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [vK : Valued K ℤₘ₀] [Valuation.IsDiscrete vK.v] [vL : Valued L ℤₘ₀] [Algebra K L] [IsValExtension K L] [FiniteDimensional K L]

noncomputable def G_diff (i : ℤ) : Finset (L ≃ₐ[K] L) := ((G(L/K)_[i] : Set (L ≃ₐ[K] L)) \ (G(L/K)_[(i + 1)] : Set (L ≃ₐ[K] L))).toFinset
noncomputable def Ramification_Group_diff (i : ℤ) : Finset (L ≃ₐ[K] L) := ((G(L/K)_[i] : Set (L ≃ₐ[K] L)) \ (G(L/K)_[(i + 1)] : Set (L ≃ₐ[K] L))).toFinset
@@ -263,7 +382,7 @@ theorem Ramification_Group_pairwiseDisjoint (n : ℤ) : (PairwiseDisjoint (↑(F
rintro i _ j _ hij u hu1 hu2
have hu : u ≤ (Ramification_Group_diff K L i) ∩ (Ramification_Group_diff K L j) := by
rintro s hs
simp
simp only [Finset.mem_inter]
constructor
· apply mem_of_subset_of_mem hu1 hs
· apply mem_of_subset_of_mem hu2 hs
@@ -272,178 +391,115 @@ theorem Ramification_Group_pairwiseDisjoint (n : ℤ) : (PairwiseDisjoint (↑(F
simp at hs
apply Ramification_Group_Disjoint K L hs.1 hs.2 hij

--i don't know how to name them
theorem x_not_in_aux {x : (L ≃ₐ[K] L)} (hx : x ≠ .refl) : ∃ (n : ℤ) , x ∉ G(L/K)_[n] := by sorry
set_option synthInstance.maxHeartbeats 0

variable [CompleteSpace K] [Algebra.IsSeparable K L] [Algebra.IsSeparable (LocalRing.ResidueField ↥𝒪[K]) (LocalRing.ResidueField ↥𝒪[L])]

theorem x_in_G_n {x : (L ≃ₐ[K] L)} (hx : x ≠ .refl) : ∃ (n : ℤ) , -1 ≤ n ∧ x ∈ G(L/K)_[n] ∧ x ∉ G(L/K)_[(n + 1)] := by
by_contra hc
push_neg at *
obtain ⟨n, hn⟩ := x_not_in_aux K L hx
apply hn
sorry
theorem mem_all_lowerRamificationGroup_iff_refl {x : (L ≃ₐ[K] L)}: (∀ n : ℤ, x ∈ G(L/K)_[n]) ↔ x = .refl := by
constructor <;> intro h
· by_contra hc
push_neg at hc
have hx : x = AlgEquiv.refl := by
obtain ⟨u, hu⟩ := exist_lowerRamificationGroup_eq_bot (K := K) (L := L)
replace h : x ∈ G(L/K)_[u] := by apply h u
rw [hu] at h
apply Subgroup.mem_bot.1 h
apply hc hx
· intro n
rw [h]
apply Subgroup.one_mem

theorem mem_all_lowerRamificationGroup_iff {x : (L ≃ₐ[K] L)}: (∀ n : ℤ, x ∈ G(L/K)_[n]) ↔ x = .refl := by
constructor
<;>rintro h
have htop : i_[L/K] x = ⊤ := by
by_contra hc
simp at hc
push_neg at *
obtain ⟨m, hx, hx', hx''⟩ := x_in_G_n K L sorry -- hc
apply hx''
apply h
sorry
sorry
-- apply lowerIndex_eq_top_iff_eq_refl.1 htop
-- rintro n
-- have : x ∈ G(L/K)_[n.toNat] := by
-- apply (mem_lowerRamificationGroup_iff n.toNat).2
-- rw [h, (lowerIndex_refl (R := K) (S := L))]
-- simp
-- sorry

theorem m_lt_n_of_in_G_m_of_notin_G_n {x : (L ≃ₐ[K] L)} {m n : ℤ} (hm : x ∈ G(L/K)_[m]) (hn : x ∉ G(L/K)_[n]) : m ≤ n - 1 := by
by_contra hc
push_neg at *
have h : G(L/K)_[m] ≤ G(L/K)_[n] := by
convert lowerRamificationGroup.antitone K L hc
simp
simp only [sub_add_cancel]
apply hn
apply Set.mem_of_subset_of_mem h hm

theorem G_n_or_G_lt_n {n : ℤ} {x : (L ≃ₐ[K] L)} (h : x ∉ G(L/K)_[n]) : ∃ a, (-1 ≤ a ∧ a ≤ n - 1) ∧ x ∈ G_diff K L a := by
have hx : x ≠ .refl := by
by_contra hc
have : x ∈ G(L/K)_[n] := by apply (mem_all_lowerRamificationGroup_iff K L).2 hc
contradiction
obtain ⟨m, ⟨hmgt, hx, hx'⟩⟩ := (x_in_G_n K L hx)
have hm' : m ≤ n - 1 := by apply m_lt_n_of_in_G_m_of_notin_G_n K L hx h
have hx'' : x ∈ G_diff K L m := by simp [G_diff, hx, hx']
use m
theorem aux_0 {x : L ≃ₐ[K] L} (hx : x ≠ .refl) : ∃ n : ℤ , x ∈ G(L/K)_[n] ∧ x ∉ G(L/K)_[(n + 1)] := by
by_contra hc; push_neg at hc
apply hx
apply (mem_all_lowerRamificationGroup_iff_refl K L).1
intro n
set t := n + 1; have : n = t - 1 := by ring
rw [this]
induction' t using Int.induction_on with m hm m hm
· simp only [zero_sub, reduceNeg]
rw [lowerRamificationGroup_eq_decompositionGroup, decompositionGroup_eq_top]
apply Subgroup.mem_top; rfl
· have : ((m : ℤ) + 1 - 1) = ((m : ℤ) - 1 + 1) := by simp only [add_sub_cancel_right,
sub_add_cancel]
rw [this]
apply hc (m - 1) hm
· rw [lowerRamificationGroup_eq_decompositionGroup, decompositionGroup_eq_top]
apply Subgroup.mem_top
simp only [reduceNeg, tsub_le_iff_right, add_left_neg, zero_add]
omega

theorem Raimification_Group_split (n : ℤ) : (⊤ : Finset (L ≃ₐ[K] L)) = (disjiUnion (Finset.Icc (-1) (n - 1)) (Ramification_Group_diff K L) (Ramification_Group_pairwiseDisjoint K L n)) ∪ (G(L/K)_[n] : Set (L ≃ₐ[K] L)).toFinset := by
ext x
constructor
simp
by_cases h : x ∈ G(L/K)_[n]
· right
assumption
left
apply G_n_or_G_lt_n K L h
simp

-- theorem Sum_Trunc_lower_Index_of_G_n (n : ℤ) (u : ℚ) (h : u ≤ n) : (Finset.sum (G(L/K)_[n] : Set (L ≃ₐ[K] L)).toFinset ((AlgEquiv.truncatedLowerIndex K L (u + 1) ·))) = (u + 1) * (Nat.card (G(L/K)_[n])) := by
-- calc
-- _ = Finset.sum (G(L/K)_[n] : Set (L ≃ₐ[K] L)).toFinset (fun (x : _) => u + 1) := by
-- apply sum_equiv (.refl (L ≃ₐ[K] L))
-- simp
-- rintro s hs
-- sorry
-- _ = (u + 1) * (Nat.card (G(L/K)_[n])) := by
-- norm_num
-- ring

-- theorem Sum_Trunc_lower_Index_of_diff_G (n : ℤ) (u : ℚ) (h : n ≤ u) : (Finset.sum (G_diff K L n) ((AlgEquiv.truncatedLowerIndex K L (u + 1) ·))) = (n + 1) * (Nat.card (G_diff K L n)) := by
-- calc
-- _ = (Finset.sum (G_diff K L n) (fun (x : _) => ((n : ℚ) + 1))) := by
-- apply sum_equiv (.refl (L ≃ₐ[K] L))
-- simp
-- rintro s hs
-- sorry
-- _ = (n + 1) * (Nat.card (G_diff K L n)) := by
-- norm_num
-- ring

theorem relindex_aux {u : ℚ} : relindex G(L/K)_[⌈u⌉] G(L/K)_[0] = (Nat.card G(L/K)_[0]) / Nat.card G(L/K)_[⌈u⌉] := by sorry

theorem phi_eq_sum_card {u : ℚ} : phi K L u = (1 / Nat.card G(L/K)_[0]) * ((∑ x in Finset.Icc 1 (⌈u⌉ - 1), Nat.card G(L/K)_[x]) + (u - (max 0 (⌈u⌉ - 1))) * (Nat.card G(L/K)_[⌈u⌉])) := by
unfold phi phiDeriv
calc
_ = ∑ x in Finset.Icc 1 (⌈u⌉ - 1), ((1 : ℚ) / Nat.card G(L/K)_[0]) * (Nat.card G(L/K)_[x]) + (u - (max 0 (⌈u⌉ - 1))) * (1 / (relindex G(L/K)_[⌈u⌉] G(L/K)_[0])) := by
congr
ext x
rw [relindex_aux, div_mul_eq_mul_div, one_mul, Nat.cast_div, one_div_div]
simp
· simp
rw [← Nat.card_eq_fintype_card]
sorry
-- apply Subgroup.card_dvd_of_le
--sorry
--apply lowerRamificationGroup.antitone
--sorry
· sorry
_ = ((1 : ℚ) / Nat.card G(L/K)_[0]) * (∑ x in Finset.Icc 1 (⌈u⌉ - 1), Nat.card G(L/K)_[x]) + (u - (max 0 (⌈u⌉ - 1))) * (1 / ↑(relindex G(L/K)_[⌈u⌉] G(L/K)_[0])) := by
rw [(Finset.mul_sum (Finset.Icc 1 (⌈u⌉ - 1)) (fun i => (Nat.card (lowerRamificationGroup K L i) : ℚ)) ((1 : ℚ) / Nat.card G(L/K)_[0])).symm]
simp
_ = (1 / Nat.card G(L/K)_[0]) * ((∑ x in Finset.Icc 1 (⌈u⌉ - 1), Nat.card G(L/K)_[x]) + (u - (max 0 (⌈u⌉ - 1))) * (Nat.card G(L/K)_[⌈u⌉])) := by
--simp [relindex_aux, mul_add]
-- rw [Nat.cast_div, inv_div, div_eq_mul_inv]
-- ring
sorry--; sorry

theorem insert_Icc_left (a b : ℤ) (ha : a ≤ b): Finset.Icc a b = insert a (Finset.Icc (a + 1) b) := by
ext x
constructor
· intro h
obtain ⟨h1, h2⟩ := Finset.mem_Icc.1 h
rw [Finset.insert_eq]
apply Finset.mem_union.2
by_cases h : x = a
· simp
by_cases hc : x ∉ G(L/K)_[n]
· left
simp [h]
· right
push_neg at *
apply Finset.mem_Icc.2
unfold Ramification_Group_diff
have h : x ≠ .refl := by
by_contra hc1
apply hc
apply (mem_all_lowerRamificationGroup_iff_refl K L).2 hc1
obtain ⟨t, ht1, ht2⟩ := aux_0 K L h
use t
constructor
· apply Int.le_of_sub_one_lt
simp [lt_of_le_of_ne h1 h.symm]
exact h2
· rw [Finset.insert_eq, Finset.mem_union, Finset.mem_Icc, Finset.mem_Icc]
rintro h
rcases h with h | ⟨h1, h2⟩
· constructor
· apply le_of_eq (Finset.mem_singleton.1 h).symm
· apply le_trans (le_of_eq (Finset.mem_singleton.1 h)) ha
· constructor
· linarith [h1]
· exact h2
· constructor
--the index is greater than -1
· sorry
· apply m_lt_n_of_in_G_m_of_notin_G_n K L ht1 hc
· simp only [toFinset_diff, mem_sdiff, mem_toFinset, SetLike.mem_coe, ht1, ht2,
not_false_eq_true, and_self]
· push_neg at hc
right; exact hc
· intro h
simp only [Finset.top_eq_univ, Finset.mem_univ]

theorem insert_Icc_right (a b : ℤ) (h : a ≤ b) : Finset.Icc a b = insert b (Finset.Icc a (b - 1)) := by
apply Finset.Subset.antisymm
· intro x hx
rw [Finset.insert_eq b (Finset.Icc a (b - 1))]
apply Finset.mem_union.2
by_cases h : x = b
· left
simp [h]
· right
simp at hx
simp
constructor
· exact hx.1
· apply Int.le_of_sub_one_lt
apply lt_of_le_of_ne
linarith
push_neg at h
simp [h]
· rw [Finset.insert_eq b (Finset.Icc a (b - 1))]
apply Finset.union_subset
simp [h]
apply Finset.Icc_subset_Icc
rfl; linarith
theorem aabb (a b : ℚ) : (1 / a) * b = b / a := by exact one_div_mul_eq_div a b

theorem sum_insert_left_aux (a b : ℤ) (ha : a ≤ b) (f : ℤ → ℕ) : (∑ x in Finset.Icc a b, f x) - f a = (∑ x in Finset.Icc (a + 1) b, f x):= by
theorem phi_eq_sum_card {u : ℚ} (hu : 0 < u): phi K L u = (1 / Nat.card G(L/K)_[0]) * ((∑ x in Finset.Icc 1 (⌈u⌉ - 1), Nat.card G(L/K)_[x]) + (u - (max 0 (⌈u⌉ - 1))) * (Nat.card G(L/K)_[⌈u⌉])) := by
unfold phi phiDeriv
calc
_ = ∑ x in insert a (Finset.Icc (a + 1) b), f x - f a := by
rw [insert_Icc_left _ _ ha]
_ = (∑ x in Finset.Icc (a + 1) b, f x) := by simp
_ = ∑ x ∈ Finset.Icc 1 (⌈u⌉ - 1), (Nat.card G(L/K)_[⌈x⌉] : ℚ) / (Nat.card G(L/K)_[0] : ℚ) + (u - (max 0 (⌈u⌉ - 1))) * ((Nat.card G(L/K)_[⌈u⌉] ) / (Nat.card G(L/K)_[0] )) := by
have h1 : ∑ x ∈ Finset.Icc 1 (⌈u⌉ - 1), (Nat.card G(L/K)_[(max 0 ⌈(x : ℚ)⌉)] : ℚ) / (Nat.card G(L/K)_[0] : ℚ) = ∑ x ∈ Finset.Icc 1 (⌈u⌉ - 1), (Nat.card G(L/K)_[⌈x⌉] : ℚ) / (Nat.card G(L/K)_[0] : ℚ) := by
have h : ∀ i ∈ Finset.Icc 1 (⌈u⌉ - 1), max 0 ⌈(i : ℚ)⌉ = ⌈i⌉ := by
intro i hi
simp only [ceil_intCast, ceil_int, id_eq, max_eq_right_iff]
rw [Finset.mem_Icc] at hi; linarith [hi.1]
apply (Finset.sum_eq_sum_iff_of_le ?_).2
· intro i hi
rw [h i hi]
· intro i hi
rw [h i hi]
have h2 : (u - (max 0 (⌈u⌉ - 1))) * ((Nat.card G(L/K)_[(max 0 ⌈u⌉)] : ℚ) / (Nat.card G(L/K)_[0] : ℚ)) = (u - (max 0 (⌈u⌉ - 1))) * ((Nat.card G(L/K)_[⌈u⌉] : ℚ) / (Nat.card G(L/K)_[0] : ℚ)) := by
have h : max 0 ⌈u⌉ = ⌈u⌉ := by
apply max_eq_right
apply le_of_lt; apply ceil_pos.2; exact hu
rw [h]
rw [h1, h2]
_ = (1 / (Nat.card G(L/K)_[0] )) * ∑ x ∈ Finset.Icc 1 (⌈u⌉ - 1), (Nat.card G(L/K)_[⌈x⌉] ) + (u - (max 0 (⌈u⌉ - 1))) * ((Nat.card G(L/K)_[⌈u⌉] ) / (Nat.card G(L/K)_[0] )) := by
congr
convert (Finset.sum_div (Finset.Icc 1 (⌈u⌉ - 1)) (fun x => (Nat.card (lowerRamificationGroup K L ⌈x⌉) : ℚ)) (Nat.card ↥ G(L/K)_[0] : ℚ))
· exact
Eq.symm (sum_div (Finset.Icc 1 (⌈u⌉ - 1)) (fun i ↦ (Nat.card ↥ G(L/K)_[⌈i⌉] : ℚ)) (Nat.card ↥ G(L/K)_[0] : ℚ))
· convert one_div_mul_eq_div (Nat.card G(L/K)_[0] : ℚ) ((∑ x ∈ Finset.Icc 1 (⌈u⌉ - 1), Nat.card ↥ G(L/K)_[⌈x⌉]) : ℚ)
· exact Nat.cast_sum (Finset.Icc 1 (⌈u⌉ - 1)) fun x ↦ Nat.card ↥ G(L/K)_[⌈x⌉]
· exact
Eq.symm (sum_div (Finset.Icc 1 (⌈u⌉ - 1)) (fun i ↦ (Nat.card ↥ G(L/K)_[⌈i⌉] : ℚ)) (Nat.card ↥ G(L/K)_[0] : ℚ))
_ = (1 / Nat.card G(L/K)_[0]) * ((∑ x in Finset.Icc 1 (⌈u⌉ - 1), Nat.card G(L/K)_[x]) + (u - (max 0 (⌈u⌉ - 1))) * (Nat.card G(L/K)_[⌈u⌉])) := by
rw [mul_add]
congr 1
rw [← mul_assoc, mul_comm (1 / (Nat.card G(L/K)_[0] : ℚ)), mul_assoc, one_div_mul_eq_div]

theorem sum_insert_left_aux' (a b : ℤ) (h : a ≤ b) (f : ℤ → ℤ) : (∑ x in Finset.Icc a b, f x) - f a = (∑ x in Finset.Icc (a + 1) b, f x) := by
calc
_ = ∑ x in insert a (Finset.Icc (a + 1) b), f x - f a := by
rw [insert_Icc_left _ _ h]
_ = (∑ x in Finset.Icc (a + 1) b, f x) := by simp

theorem sum_insert_right_aux' (a b : ℤ) (h : a ≤ b) (f : ℤ → ℤ) : (∑ x in Finset.Icc a b, f x) = (∑ x in Finset.Icc a (b - 1), f x) + f b := by
calc
@@ -472,47 +528,48 @@ theorem sum_sub_aux {u : ℚ} (hu : 0 ≤ ⌈u⌉ - 1): (∑ i in Finset.Icc (-1
invFun := fun x => x - 1
left_inv := by
rintro x
simp
simp only [add_sub_cancel_right]
right_inv := by
rintro x
simp
simp only [sub_add_cancel]
}
apply sum_equiv e
rintro i
constructor
· simp
· simp only [reduceNeg, Finset.mem_Icc, and_imp]
intro hi1 hi2
simp [e]
simp only [Equiv.coe_fn_mk, add_one_le_ceil_iff, e]
constructor
· linarith [hi1]
· apply add_one_le_ceil_iff.1 (by linarith [hi2])
· simp
· simp only [Finset.mem_Icc, reduceNeg, and_imp]
intro hi
simp [e] at *
simp only [sub_nonneg, one_le_ceil_iff, Equiv.coe_fn_mk, add_one_le_ceil_iff, reduceNeg,
e] at *
intro hi'
constructor
· linarith [hi]
· linarith [add_one_le_ceil_iff.2 hi']
rintro i hi
simp [e]
simp only [Nat.card_eq_fintype_card, Equiv.coe_fn_mk, e]
_ = ((-1) + 1) * Nat.card G(L/K)_[(-1)] + ∑ i in Finset.Icc 0 (⌈u⌉ - 1), (i + 1) * Nat.card G(L/K)_[i] - ∑ i in Finset.Icc 0 (⌈u⌉ - 1), i * Nat.card G(L/K)_[i] - ⌈u⌉ * Nat.card G(L/K)_[⌈u⌉] := by
have h : (-1) ≤ ⌈u⌉ - 1 := by linarith [hu]
erw [← sum_insert_left_aux' (-1) (⌈u⌉ - 1) h (fun i => (i + 1) * Nat.card (lowerRamificationGroup K L i)), sub_sub, ← sum_insert_right_aux' 0 ⌈u⌉ (by linarith [h]) (fun i => i * Nat.card (lowerRamificationGroup K L i))]
simp
_ = ∑ i in Finset.Icc 0 (⌈u⌉ - 1), Nat.card G(L/K)_[i] - ⌈u⌉ * (Nat.card G(L/K)_[⌈u⌉]) := by
sorry
-- rw [neg_add_self, zero_mul, zero_add]
-- congr
-- rw [← sum_sub_distrib]
-- ring_nf
-- simp
rw [neg_add_self, zero_mul, zero_add]
congr
rw [← sum_sub_distrib]
ring_nf
exact Eq.symm (Nat.cast_sum (Finset.Icc 0 (-1 + ⌈u⌉)) fun x ↦ Nat.card ↥ G(L/K)_[x])

theorem truncatedLowerindex_eq_if {i : ℤ} {u : ℚ} {s : (L ≃ₐ[K] L)} (hu : i ≤ (⌈u⌉ - 1)) (hs : s ∈ Ramification_Group_diff K L i) : i_[L/K]ₜ (u + 1) s = i + 1 := by
unfold Ramification_Group_diff at hs
simp at hs
rcases hs with ⟨hs1, hs2⟩
sorry


theorem sum_of_diff_aux {i : ℤ} {u : ℚ} (h : i ∈ Finset.Icc (-1) (⌈u⌉ - 1)) : ∑ s in Ramification_Group_diff K L i, (AlgEquiv.truncatedLowerIndex K L (u + 1) s) = (i + 1) * (Nat.card G(L/K)_[i] - Nat.card G(L/K)_[(i + 1)]) := by
calc
∑ s in Ramification_Group_diff K L i, (AlgEquiv.truncatedLowerIndex K L (u + 1) s) = ∑ s in Ramification_Group_diff K L i, ((i : ℚ) + 1) := by
@@ -532,7 +589,7 @@ theorem sum_of_diff_aux {i : ℤ} {u : ℚ} (h : i ∈ Finset.Icc (-1) (⌈u⌉
rw [toFinset_diff, card_sdiff (by apply Set.toFinset_mono hsub)]
simp
rw [h, Nat.cast_sub]
sorry
exact Set.card_le_card hsub


--for lower numbering
@@ -607,7 +664,7 @@ theorem phi_eq_sum_inf (u : ℚ) : (phi K L u) = (1 / Nat.card G(L/K)_[0]) * ((F
simp [add_one_le_ceil_iff.2 hu, hu]
calc
_ = (1 / Nat.card G(L/K)_[0]) * ((∑ i in Finset.Icc 1 (⌈u⌉ - 1), Nat.card G(L/K)_[i]) + (u - (max 0 (⌈u⌉ - 1))) * (Nat.card G(L/K)_[⌈u⌉])) := by
apply phi_eq_sum_card K L
apply phi_eq_sum_card K L (by linarith [hu])
_ = (1 / Nat.card G(L/K)_[0]) * ((∑ i in Finset.Icc 0 (⌈u⌉ - 1), Nat.card G(L/K)_[i]) + (u - (max 0 (⌈u⌉ - 1))) * (Nat.card G(L/K)_[⌈u⌉])) - (1 : ℕ) := by
have h : 0 < Nat.card G(L/K)_[0] := by sorry
erw [← sum_insert_left_aux 0 (⌈u⌉ - 1) hu' (fun x => Nat.card (lowerRamificationGroup K L x)), ← (Nat.div_self h), Nat.cast_div (by simp) (by sorry -- simp [h]
338 changes: 338 additions & 0 deletions RamificationGroup/Herbrand_aux.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,338 @@
import RamificationGroup.HerbrandFunction
import Mathlib.RingTheory.Valuation.Basic

open scoped Classical
open HerbrandFunction DiscreteValuation AlgEquiv Valued
open DiscreteValuation Subgroup Set Function Finset BigOperators Int Valued

variable (K L : Type*) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [vK : Valued K ℤₘ₀] [Valuation.IsDiscrete vK.v] [vL : Valued L ℤₘ₀] [Algebra K L] [IsValExtension K L] [FiniteDimensional K L] [CompleteSpace K] [Algebra.IsSeparable K L]
[Algebra.IsSeparable (LocalRing.ResidueField ↥𝒪[K]) (LocalRing.ResidueField ↥𝒪[L])]

theorem Int.aux {a b : ℤ} (h1 : a ≤ b) (h2 : b < a + 1) : a = b := by
by_contra hc
have h3 : a < b := by exact lt_of_le_of_ne h1 hc
have h4 : a + 1 ≤ b := by exact h3
absurd h4; push_neg; exact h2

set_option maxHeartbeats 0

theorem truncatedLowerindex_eq_if_aux {i : ℤ} {u : ℚ} {s : (L ≃ₐ[K] L)} (hgt : 0 ≤ u) (hgt' : -1 ≤ i) (hu : i ≤ (⌈u⌉ - 1)) (hs : s ∈ HerbrandFunction.Ramification_Group_diff K L i) {gen : 𝒪[L]} (hgen : Algebra.adjoin 𝒪[K] {gen} = ⊤) : i_[L/K]ₜ (u + 1) s = i + 1 := by
unfold Ramification_Group_diff at hs
simp only [Set.toFinset_diff, Finset.mem_sdiff, Set.mem_toFinset, SetLike.mem_coe] at hs
rcases hs with ⟨hs1, hs2⟩
have h1 : i + 1 ≤ i_[L/K]ₜ (u + 1) s := by
have h1' : i ≤ i_[L/K]ₜ (u + 1) s - 1 := by
apply (le_truncatedLowerIndex_sub_one_iff_mem_lowerRamificationGroup s i (u + 1) _ hgen).2
· simp only [ceil_intCast, hs1]
· simp only [add_le_add_iff_right]
apply le_of_lt; apply Int.add_one_le_ceil_iff.1; linarith [hu]
linarith [h1']
have h2 : i_[L/K]ₜ (u + 1) s < i + 2 := by
by_contra hc; push_neg at hc
have h : s ∈ decompositionGroup K L := by exact mem_decompositionGroup s
have hs2' : s ∈ G(L/K)_[⌈i + 1⌉] := by
convert mem_lowerRamificationGroup_of_le_truncatedLowerIndex_sub_one h (u := ((i : ℤ) + 1)) (by linarith [hc])
simp only [ceil_add_one, ceil_int, id_eq, ceil_intCast]
apply hs2
simp only [ceil_add_one, ceil_int, id_eq] at hs2'; exact hs2'
have h3 : i_[L/K] s ≠ ⊤ := by
by_contra hc
rw [lowerIndex_eq_top_iff_eq_refl (by apply mem_decompositionGroup)] at hc
have hs2' : s ∈ G(L/K)_[(i + 1)] := by
rw [hc]; apply Subgroup.one_mem
apply hs2 hs2'
have h4 : i_[L/K]ₜ (u + 1) s = ↑(WithTop.untop (i_[L/K] s) (of_eq_false (eq_false h3) : ¬ i_[L/K] s = ⊤)) := by
unfold AlgEquiv.truncatedLowerIndex
simp only [h3, ↓reduceDIte, min_eq_right_iff, ge_iff_le]
apply le_of_lt
-- have h : i_[L/K] s < i.toNat + 1 + 1 := by
-- by_contra hc; push_neg at hc
-- have hs2' : s ∈ G(L/K)_[(i.toNat + 1)] := by
-- apply (mem_lowerRamificationGroup_iff_of_generator (K := K) (L := L) hgen (s := s) ?_ (i.toNat + 1)).2 hc
-- · apply mem_decompositionGroup s
-- by_cases hc : 0 ≤ i
-- · rw [Int.toNat_of_nonneg hc] at hs2'
-- apply hs2 hs2'
-- · have hi : i = -1 := by
-- symm
-- apply eq_iff_le_not_lt.2
-- constructor
-- · exact hgt'
-- · linarith [hc]
-- simp only [hi, reduceNeg, reduceToNat, CharP.cast_eq_zero, zero_add] at hs2'
-- simp only [hi, reduceNeg, add_left_neg] at hs2
-- have hs2'' : s ∈ G(L/K)_[0] := by
-- apply mem_of_subset_of_mem ?_ hs2'
-- apply lowerRamificationGroup.antitone
-- linarith
-- apply hs2 hs2''
have h : i_[L/K] s < (i + 1).toNat + 1 := by
by_contra hc
push_neg at hc
have hi : 0 ≤ i + 1 := by linarith [hgt']
have hs2' : s ∈ G(L/K)_[(i + 1).toNat] := by
apply (mem_lowerRamificationGroup_iff_of_generator hgen ?_ (i + 1).toNat).2
exact hc
apply mem_decompositionGroup s
rw [Int.toNat_of_nonneg hi] at hs2'
apply hs2 hs2'
have h' : (i + 1).toNat ≤ i_[L/K] s := by
by_contra hc
push_neg at hc
have h1' : i_[L/K]ₜ (u + 1) s < i + 1 := by
unfold AlgEquiv.truncatedLowerIndex
simp only [h3, ↓reduceDIte, min_lt_iff, add_lt_add_iff_right]
right
rw [← Int.cast_one, ← cast_add, ← Int.cast_natCast, cast_lt, ← Int.toNat_of_nonneg (a := i + 1), Nat.cast_lt]
apply (WithTop.untop_lt_iff _).2
exact hc
linarith [hgt']
absurd h1
push_neg
exact h1'
have hilk : i_[L/K] s = (i + 1).toNat := by
by_cases hc : 1 ≤ i + 1
· apply (ENat.toNat_eq_iff _).1
apply Nat.eq_of_lt_succ_of_not_lt
· rw [← Nat.cast_lt (α := ℕ∞), ENat.coe_toNat h3, Nat.cast_add, Nat.cast_one]
exact h
· push_neg
rw [← Nat.cast_le (α := ℕ∞), ENat.coe_toNat h3]
exact h'
simp only [ne_eq, toNat_eq_zero, not_le]
linarith [hc]
· have hi : i = -1 := by
symm; apply eq_iff_le_not_lt.2; constructor
· exact hgt'
· linarith [hc]
simp only [hi, reduceNeg, add_left_neg, toNat_zero, CharP.cast_eq_zero]
by_contra hcon
have hilk : 1 ≤ i_[L/K] s := by
apply ENat.one_le_iff_ne_zero.2 hcon
simp only [hi, reduceNeg, add_left_neg, toNat_zero, CharP.cast_eq_zero, zero_add] at h
absurd h; push_neg
exact hilk
apply lt_of_le_of_lt (b := (⌈u⌉.toNat : ℚ))
· rw [Nat.cast_le]
apply (WithTop.untop_le_iff h3).2
rw [hilk, ENat.some_eq_coe, Nat.cast_le]
apply toNat_le_toNat
linarith [hu]
· rw [← Int.cast_natCast, Int.toNat_of_nonneg]
exact ceil_lt_add_one u
exact ceil_nonneg hgt
-- by_cases hc : 0 ≤ i
-- · have hilk : i_[L/K] s = i.toNat + 1 := by
-- have h' : i.toNat + 1 ≤ i_[L/K] s := by sorry
-- rw [← Nat.cast_one, ← Nat.cast_add]
-- apply (ENat.toNat_eq_iff _).1
-- apply Nat.eq_of_lt_succ_of_not_lt
-- · sorry
-- · sorry
-- simp only [ne_eq, add_eq_zero, toNat_eq_zero, one_ne_zero, and_false, not_false_eq_true]
-- have hilk' : i_[L/K] s ≤ ⌈u⌉.toNat := by
-- rw [hilk, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le, ← Nat.cast_le (α := ℤ), Nat.cast_add, Int.toNat_of_nonneg hc, Int.toNat_of_nonneg, Nat.cast_one]
-- linarith [hu]
-- exact ceil_nonneg hgt
-- apply lt_of_le_of_lt (b := (⌈u⌉.toNat : ℚ))
-- · simp only [Nat.cast_le]
-- apply (WithTop.untop_le_iff h3).2
-- exact hilk'
-- · rw [← Int.cast_natCast, Int.toNat_of_nonneg]
-- exact ceil_lt_add_one u
-- exact ceil_nonneg hgt
-- · have hi : i = -1 := by
-- symm
-- apply eq_iff_le_not_lt.2
-- constructor
-- · exact hgt'
-- · linarith [hc]
-- have hilk : i_[L/K] s = 0 := by
-- sorry
-- simp only [hilk, WithTop.untop_zero, CharP.cast_eq_zero, gt_iff_lt]
-- exact add_pos_of_nonneg_of_pos hgt rfl
-- have h' : i_[L/K] s < ⌈u⌉.toNat + 1 := by
-- apply lt_of_lt_of_le h
-- by_cases hc : 0 ≤ i
-- · sorry
-- · have hi : i = -1 := by
-- symm
-- apply eq_iff_le_not_lt.2
-- constructor
-- · exact hgt'
-- · linarith [hc]
-- simp only [hi, reduceNeg, reduceToNat, CharP.cast_eq_zero, zero_add, ge_iff_le]
-- sorry
-- apply Int.lt_ceil.1
-- rw [ceil_add_one, ← Int.toNat_of_nonneg (a := ⌈u⌉) _, ← Nat.cast_one, ← Nat.cast_add, ofNat_eq_coe, Nat.cast_lt]
-- apply (WithTop.untop_lt_iff h3).2
-- simp only [WithTop.coe_add, ENat.some_eq_coe, WithTop.coe_one, h']
-- exact ceil_nonneg hgt
-- have h' : (WithTop.untop (i_[L/K] s) (of_eq_false (eq_false h3) : ¬ i_[L/K] s = ⊤)) < ⌈u⌉.toNat := by
-- apply lt_of_lt_of_le (b := i.toNat + 1)
-- · apply (WithTop.untop_lt_iff h3 (b := i.toNat + 1)).2; simp only [WithTop.coe_add, ENat.some_eq_coe, WithTop.coe_one, h]
-- · rw [← Nat.cast_le (α := ℤ), Nat.cast_add, Int.toNat_of_nonneg (by apply ceil_nonneg hgt'), Int.toNat_of_nonneg (by apply ceil_nonneg hgt), Nat.cast_one]
-- linarith [hu]
-- apply lt_of_lt_of_le (b := (⌈u⌉.toNat : ℚ))
-- · simp only [Nat.cast_lt, h']
-- · have h1 : ⌈u⌉ ≤ u + 1 := by
-- linarith [ceil_lt_add_one u]
-- rw [← Int.cast_natCast, Int.toNat_of_nonneg ?_]; exact h1
-- simp only [ceil_nonneg hgt]
rw [h4, ← cast_one, ← cast_add (m := i) (n := 1)]
have : (2 : ℚ) = ((2 : ℤ) : ℚ) := by simp only [cast_ofNat]
rw [h4] at h1 h2
have h5 : (WithTop.untop (i_[L/K] s) (of_eq_false (eq_false h3) : ¬ i_[L/K] s = ⊤)) = i + 1 := by
symm
apply Int.aux
· rw [← cast_one, ← cast_add (m := i) (n := 1), ← Int.cast_natCast, cast_le] at h1
exact h1
· have h : (2 : ℚ) = ((2 : ℤ) : ℚ) := by simp only [cast_ofNat]
rw [h , ← cast_add (m := i) (n := 2), ← Int.cast_natCast, cast_lt] at h2
rw [add_assoc, one_add_one_eq_two]; exact h2
exact Rat.ext h5 rfl

theorem sum_of_diff_aux_aux {i : ℤ} {u : ℚ} (h : i ∈ Finset.Icc (-1) (⌈u⌉ - 1)) : ∑ s in Ramification_Group_diff K L i, (AlgEquiv.truncatedLowerIndex K L (u + 1) s) = (i + 1) * (Nat.card G(L/K)_[i] - Nat.card G(L/K)_[(i + 1)]) := by
calc
∑ s in Ramification_Group_diff K L i, (AlgEquiv.truncatedLowerIndex K L (u + 1) s) = ∑ s in Ramification_Group_diff K L i, ((i : ℚ) + 1) := by
apply sum_equiv (by rfl : (L ≃ₐ[K] L) ≃ (L ≃ₐ[K] L)) (by simp)
intro s hs
apply truncatedLowerindex_eq_if
obtain ⟨_, h2⟩ := Finset.mem_Icc.1 h
exact h2
exact hs
_ = (i + 1) * (Nat.card G(L/K)_[i] - Nat.card G(L/K)_[(i + 1)]) := by
simp only [sum_const, smul_add, nsmul_eq_mul, mul_comm, mul_one, Nat.card_eq_fintype_card,
add_mul, one_mul]
unfold Ramification_Group_diff
have hsub : (G(L/K)_[(i + 1)] : Set (L ≃ₐ[K] L)) ⊆ (G(L/K)_[i] : Set (L ≃ₐ[K] L)) := by
apply lowerRamificationGroup.antitone
linarith
have h : (((G(L/K)_[i] : Set (L ≃ₐ[K] L)) \ (G(L/K)_[(i + 1)] : Set (L ≃ₐ[K] L))).toFinset).card = ((Fintype.card G(L/K)_[i] ) - (Fintype.card G(L/K)_[(i + 1)])) := by
rw [toFinset_diff, card_sdiff (by apply Set.toFinset_mono hsub)]
simp only [toFinset_card, SetLike.coe_sort_coe]
rw [h, Nat.cast_sub]
exact Set.card_le_card hsub

theorem truncatedLowerindex_eq_of_lt {s : (L ≃ₐ[K] L)} {u : ℚ} (h : s ∈ G(L/K)_[⌈u⌉]) (hu : 0 ≤ u) {gen : 𝒪[L]} (hgen : Algebra.adjoin 𝒪[K] {gen} = ⊤) : i_[L/K]ₜ (u + 1) s = u + 1 := by
unfold AlgEquiv.truncatedLowerIndex
by_cases ht : i_[L/K] s = ⊤
· simp only [ht, ↓reduceDIte]
· simp only [ht, ↓reduceDIte, min_eq_left_iff]
have h1 : ⌈u⌉.toNat + 1 ≤ i_[L/K] s := by
apply (mem_lowerRamificationGroup_iff_of_generator hgen ?_ ⌈u⌉.toNat).1
rw [Int.toNat_of_nonneg]; exact h; exact ceil_nonneg hu
· apply mem_decompositionGroup
have h2 : u + 1 ≤ ⌈u⌉.toNat + 1 := by
apply (add_le_add_iff_right 1).2
apply le_trans (b := (⌈u⌉ : ℚ))
· exact le_ceil u
· apply Int.cast_mono; apply self_le_toNat ⌈u⌉
apply le_trans h2
have h3 : ⌈u⌉.toNat + 1 ≤ WithTop.untop (i_[L/K] s) (of_eq_false (eq_false ht) : ¬ i_[L/K] s = ⊤) := by
apply (WithTop.le_untop_iff ht).2
simp only [WithTop.coe_add, ENat.some_eq_coe, WithTop.coe_one, h1]
rw [← Mathlib.Tactic.Ring.inv_add (a₁ := ⌈u⌉.toNat) (a₂ := 1) rfl (by simp only [Nat.cast_one])]
apply Nat.mono_cast h3

set_option synthInstance.maxHeartbeats 0

theorem truncatedLowerIndex_aux (u : ℚ) (hu : 0 ≤ ⌈u⌉) (x : L ≃ₐ[K] L) (hx : x ∈ G(L/K)_[⌈u⌉]) {gen : 𝒪[L]} (hgen : Algebra.adjoin 𝒪[K] {gen} = ⊤) : i_[L/K]ₜ (⌈u⌉ + 1) x = (⌈u⌉ + 1) := by
unfold AlgEquiv.truncatedLowerIndex
by_cases hc : i_[L/K] x = ⊤
· simp only [hc, ↓reduceDIte]
· simp only [hc, ↓reduceDIte, min_eq_left_iff]
have h : ⌈u⌉.toNat + 1 ≤ WithTop.untop (i_[L/K] x) (of_eq_false (eq_false hc) : ¬ i_[L/K] x = ⊤) := by
apply (WithTop.le_untop_iff _).2
apply (mem_lowerRamificationGroup_iff_of_generator hgen ?_ ⌈u⌉.toNat).1
· rw [Int.toNat_of_nonneg]; exact hx; exact hu
· apply mem_decompositionGroup
apply le_trans (b := (⌈u⌉.toNat + 1 : ℚ))
· simp only [add_le_add_iff_right, ← Int.cast_natCast (R := ℚ) ⌈u⌉.toNat, Int.cast_mono (self_le_toNat ⌈u⌉)]
· simp only [← Nat.cast_one (R := ℚ), ← Nat.cast_add (m := ⌈u⌉.toNat) (n := 1), Nat.mono_cast h]


theorem phi_eq_sum_inf (u : ℚ) (hu : 0 ≤ u) {gen : 𝒪[L]} (hgen : Algebra.adjoin 𝒪[K] {gen} = ⊤) : (phi K L u) = (1 / Nat.card G(L/K)_[0]) * ((Finset.sum (⊤ : Finset (L ≃ₐ[K] L)) (AlgEquiv.truncatedLowerIndex K L (u + 1) ·))) - 1 := by
-- by_cases hu : u ≤ 0
-- · have hu' : ⌈u⌉ - 1 < 0 := by
-- apply lt_of_lt_of_le
-- linarith [ceil_lt_add_one u]
-- apply ceil_le.2 hu
-- rw [phi_eq_self_of_le_zero K L hu, sum_fiberwise_aux K L]
-- symm
-- by_cases huc : ⌈u⌉ < 0
-- · have huc' : ⌈u⌉ - 1 < (-1) := by linarith [huc]
-- simp only [Nat.card_eq_fintype_card, one_div, reduceNeg, huc', Finset.Icc_eq_empty_of_lt, sum_empty, zero_add, mul_comm, mul_assoc]

-- sorry
-- · have huc' : ⌈u⌉ = 0 := by omega
-- have huc'' : ⌈u⌉ - 1 = (-1) := by linarith [huc']
-- have hsum : ∑ s in Ramification_Group_diff K L (-1), i_[L/K]ₜ (u + 1) s = 0 := by
-- apply Finset.sum_eq_zero
-- intro x hx
-- simp [truncatedLowerindex_eq_if K L (by linarith [huc'']) hx]
-- simp [huc', huc'', hsum, mul_comm, mul_assoc, mul_inv_self]
-- --sorry
by_cases hc : 0 < u
· have hu' : 0 ≤ ⌈u⌉ - 1 := by
simp only [sub_nonneg, one_le_ceil_iff]; exact hc
--push_neg at hu
--simp [add_one_le_ceil_iff.2 hu, hu]
calc
_ = (1 / Nat.card G(L/K)_[0]) * ((∑ i in Finset.Icc 1 (⌈u⌉ - 1), Nat.card G(L/K)_[i]) + (u - (max 0 (⌈u⌉ - 1))) * (Nat.card G(L/K)_[⌈u⌉])) := by
apply phi_eq_sum_card K L hc
_ = (1 / Nat.card G(L/K)_[0]) * ((∑ i in Finset.Icc 0 (⌈u⌉ - 1), Nat.card G(L/K)_[i]) + (u - (max 0 (⌈u⌉ - 1))) * (Nat.card G(L/K)_[⌈u⌉])) - (1 : ℕ) := by
have h : 0 < Nat.card G(L/K)_[0] := by rw [← ceil_zero (α := ℤ)]; sorry --apply Ramification_Group_card_pos
erw [← sum_insert_left_aux 0 (⌈u⌉ - 1) hu' (fun x => Nat.card (lowerRamificationGroup K L x)), ← (Nat.div_self h), Nat.cast_div (by simp) (by simp [h]), ← (mul_one_div ((Nat.card G(L/K)_[0]) : ℚ) ((Nat.card G(L/K)_[0]) : ℚ)), (mul_comm ((Nat.card ↥ G(L/K)_[0]) : ℚ) (1 / ↑(Nat.card ↥ G(L/K)_[0] ))), ← mul_sub, Nat.cast_sub]
· ring
· rw [insert_Icc_left 0 (⌈u⌉ - 1) hu', Finset.sum_insert (by simp)]
simp only [Nat.card_eq_fintype_card, zero_add, le_add_iff_nonneg_right, zero_le]
_ = (1 / Nat.card G(L/K)_[0]) * ((∑ i in Finset.Icc (-1) (⌈u⌉ - 1), (i + 1) * (Nat.card G(L/K)_[i] - Nat.card G(L/K)_[(i + 1)])) + (u + 1) * (Nat.card G(L/K)_[⌈u⌉])) - 1 := by
rw [sum_sub_aux K L hu', cast_sub]
congr 2
have h : (u - max 0 (⌈u⌉ - 1)) * (Nat.card G(L/K)_[⌈u⌉]) = (u + 1) * (Nat.card G(L/K)_[⌈u⌉]) - ⌈u⌉ * (Nat.card G(L/K)_[⌈u⌉]) := by
simp only [hu', max_eq_right, cast_sub, cast_one, ← sub_add, Nat.card_eq_fintype_card]
ring
rw [h, add_sub, cast_mul, cast_natCast, add_comm_sub, add_sub]
congr
_ = (1 / Nat.card G(L/K)_[0]) * ((∑ i in Finset.Icc (-1) (⌈u⌉ - 1), ∑ s in Ramification_Group_diff K L i, (AlgEquiv.truncatedLowerIndex K L (u + 1) s)) + (u + 1) * (Nat.card G(L/K)_[⌈u⌉])) - 1 := by
congr 3
have h : Finset.Icc (-1) (⌈u⌉ - 1) = Finset.Icc (-1) (⌈u⌉ - 1) := by rfl
rw [Int.cast_sum]
apply sum_congr h
intro x hx
simp only [Nat.card_eq_fintype_card, cast_mul, cast_add, cast_one, cast_sub,
Int.cast_natCast, (sum_of_diff_aux K L hx)]
_ = (1 / Nat.card G(L/K)_[0]) * ((Finset.sum (⊤ : Finset (L ≃ₐ[K] L)) (AlgEquiv.truncatedLowerIndex K L (u + 1) ·))) - 1 := by
congr 2
apply (sum_fiberwise_aux K L (u := u)).symm
· have hu' : u = 0 := by apply (eq_of_le_of_not_lt hu hc).symm
rw [hu', phi_zero_eq_zero]
symm
rw [sub_eq_zero, Raimification_Group_split K L 0, sum_union]
· simp only [one_div, reduceNeg, zero_sub, Finset.Icc_self,
disjiUnion_eq_biUnion, singleton_biUnion, zero_add]
calc
_ = ((Nat.card ↥ G(L/K)_[0]) : ℚ)⁻¹ * (0 + ∑ x ∈ (G(L/K)_[0] : Set (L ≃ₐ[K] L)).toFinset, i_[L/K]ₜ 1 x) := by
-- congr
simp only [Nat.card_eq_fintype_card, reduceNeg, zero_add, _root_.mul_eq_mul_left_iff, add_left_eq_self, inv_eq_zero, Nat.cast_eq_zero, Fintype.card_ne_zero, or_false]
apply Finset.sum_eq_zero
intro x hx
rw [← zero_add 1, truncatedLowerindex_eq_if_aux K L (u := 0) (i := -1) rfl ?_ ?_ hx hgen]
simp only [reduceNeg, cast_neg, cast_one, add_left_neg]
rfl
simp only [reduceNeg, ceil_zero, zero_sub, le_refl]
_ = ((Nat.card ↥ G(L/K)_[0]) : ℚ)⁻¹ * (0 + Nat.card G(L/K)_[0]) := by
congr
have h : Nat.card G(L/K)_[0] = Finset.card (G(L/K)_[0] : Set (L ≃ₐ[K] L)).toFinset := by exact Nat.card_eq_card_toFinset (G(L/K)_[0] : Set (L ≃ₐ[K] L))
rw [h, Finset.cast_card]
apply (Finset.sum_eq_sum_iff_of_le ?_).2
<;> intro i hi
· simp only [Set.mem_toFinset] at hi
convert truncatedLowerIndex_aux K L 0 (by simp) i hi hgen
· simp only [Set.mem_toFinset] at hi
apply le_of_eq; convert truncatedLowerIndex_aux K L 0 (by simp) i hi hgen
_ = 1 := by simp only [Nat.card_eq_fintype_card, zero_add, isUnit_iff_ne_zero, ne_eq, Nat.cast_eq_zero, Fintype.card_ne_zero, not_false_eq_true, IsUnit.inv_mul_cancel]
· unfold Ramification_Group_diff
simp only [reduceNeg, zero_sub, Finset.Icc_self, toFinset_diff, disjiUnion_eq_biUnion, singleton_biUnion, add_left_neg]
exact sdiff_disjoint
29 changes: 26 additions & 3 deletions RamificationGroup/LowerNumbering.lean
Original file line number Diff line number Diff line change
@@ -384,10 +384,33 @@ theorem mem_lowerRamificationGroup_of_le_truncatedLowerIndex_sub_one {s : L ≃
convert (mem_lowerRamificationGroup_iff_of_generator sorry hs' ⌈u⌉.toNat).2 this
sorry; sorry

theorem le_truncatedLowerIndex_sub_one_iff_mem_lowerRamificationGroup (s : L ≃ₐ[K] L) (u : ℚ) (r : ℚ) (h : u + 1 ≤ r) : u ≤ i_[L/K]ₜ r s - 1 ↔ s ∈ G(L/K)_[⌈u⌉] := by
variable [IsDiscrete vK.v] [IsDiscrete vL.v] [IsValExtension K L] [CompleteSpace K] [FiniteDimensional K L]

theorem le_truncatedLowerIndex_sub_one_iff_mem_lowerRamificationGroup (s : L ≃ₐ[K] L) (u : ℚ) (r : ℚ) (h : u + 1 ≤ r) {gen : 𝒪[L]} (hgen : Algebra.adjoin 𝒪[K] {gen} = ⊤) : u ≤ i_[L/K]ₜ r s - 1 ↔ s ∈ G(L/K)_[⌈u⌉] := by
constructor
apply mem_lowerRamificationGroup_of_le_truncatedLowerIndex_sub_one
sorry; sorry
· apply mem_lowerRamificationGroup_of_le_truncatedLowerIndex_sub_one
rw [decompositionGroup_eq_top]
apply Subgroup.mem_top
· intro hs
have h1 : (⌈u⌉.toNat + 1) ≤ i_[L/K] s := by
apply (mem_lowerRamificationGroup_iff_of_generator hgen ?_ ⌈u⌉.toNat).1
--the type of N and Z make some truble
sorry
rw [decompositionGroup_eq_top]
apply Subgroup.mem_top
unfold AlgEquiv.truncatedLowerIndex
by_cases hc : i_[L/K] s = ⊤
· simp [hc]
linarith [h]
· simp [hc]
have hle : u + 1 ≤ min r ↑(WithTop.untop ( i_[L/K] s) (of_eq_false (eq_false hc) : ¬ i_[L/K] s = ⊤)) := by
apply le_min_iff.2
constructor
· exact h
· sorry
linarith [hle]



end K_is_field

0 comments on commit 04d5501

Please sign in to comment.