diff --git a/RamificationGroup/ForMathlib/LocalRing/Basic.lean b/RamificationGroup/ForMathlib/LocalRing/Basic.lean index 847554c..07af48d 100644 --- a/RamificationGroup/ForMathlib/LocalRing/Basic.lean +++ b/RamificationGroup/ForMathlib/LocalRing/Basic.lean @@ -1,4 +1,5 @@ import Mathlib.NumberTheory.RamificationInertia +import Mathlib.RingTheory.LocalRing.ResidueField.Basic namespace LocalRing diff --git a/RamificationGroup/LowerNumbering.lean b/RamificationGroup/LowerNumbering.lean index 6f7e16c..98fda92 100644 --- a/RamificationGroup/LowerNumbering.lean +++ b/RamificationGroup/LowerNumbering.lean @@ -118,8 +118,6 @@ end autCongr section WithBot -- this should be put into a suitable place, Also add `WithOne`? `WithTop`, `WithBot`, `WithOne`, `Multiplicative`, `Additive` open Classical -#check WithBot.instSupSet -#check WithTop.conditionallyCompleteLattice -- there is no `ConditionallyCompleteLinearOrderTop` in mathlib ... -- # The definition of `WithTop.instInfSet` have to be changed （done in latest version） #check WithBot.linearOrder @@ -130,15 +128,19 @@ noncomputable instance {α} [ConditionallyCompleteLinearOrder α] : Conditionall decidableEq := WithBot.decidableEq decidableLT := WithBot.decidableLT csSup_of_not_bddAbove s h := by - rw [WithBot.csSup_empty] + rw [WithBot.sSup_empty] simp only [sSup, sInf, Set.subset_singleton_iff] by_cases hs : ∀ y ∈ s, y = (⊤ : WithTop αᵒᵈ) - · rw [if_pos hs]; rfl - · rw [if_neg hs] - sorry - csInf_of_not_bddBelow := sorry + · rw [if_pos (Or.inl hs)]; rfl + · rw [show (⊤ : WithTop αᵒᵈ) = (⊥ : WithBot α) by rfl, ite_eq_left_iff] + intro h1 + push_neg at h1 + exfalso + exact h h1.2 + csInf_of_not_bddBelow s h := by + sorry bot_le := WithBot.orderBot.bot_le - csSup_empty := by simp only [WithBot.csSup_empty] + csSup_empty := by simp only [WithBot.sSup_empty] noncomputable instance {α} [ConditionallyCompleteLinearOrder α] : ConditionallyCompleteLinearOrderBot (WithZero α) := inferInstanceAs (ConditionallyCompleteLinearOrderBot (WithBot α)) @@ -256,11 +258,11 @@ variable {R : Type*} {R' S: Type*} {ΓR ΓS ΓA ΓB : outParam Type*} [CommRing @[simp] theorem lowerIndex_refl : (i_[S/R] .refl) = ⊤ := by simp only [AlgEquiv.lowerIndex, AlgEquiv.coe_refl, id_eq, sub_self, _root_.map_zero, ciSup_const, - ↓reduceDite] + ↓reduceDIte] @[simp] theorem truncatedLowerIndex_refl (u : ℚ) : AlgEquiv.truncatedLowerIndex R S u .refl = u := by - simp only [AlgEquiv.truncatedLowerIndex, lowerIndex_refl, ↓reduceDite] + simp only [AlgEquiv.truncatedLowerIndex, lowerIndex_refl, ↓reduceDIte] section lowerIndex_inequality @@ -287,7 +289,7 @@ theorem lowerIndex_ne_one {s : L ≃ₐ[K] L} (hs' : s ∈ decompositionGroup K exact sub_self_mem_integer hs' _ apply hs ext x - rcases ValuationSubring.mem_or_inv_mem 𝒪[L] x with h | h + rcases ValuationSubring.mem_or_inv_mem vL.v.valuationSubring x with h | h · exact hL ⟨x, h⟩ · calc _ = (s x⁻¹)⁻¹ := by simp only [inv_inv, map_inv₀] @@ -325,13 +327,13 @@ theorem mem_lowerRamificationGroup_iff_of_generator Set.mem_setOf_eq, AlgEquiv.lowerIndex] by_cases hrefl : s = .refl · simp only [hrefl, AlgEquiv.coe_refl, id_eq, sub_self, _root_.map_zero, ofAdd_sub, ofAdd_neg, - zero_le', implies_true, and_true, ciSup_const, ↓reduceDite, le_top, iff_true] + zero_le', implies_true, and_true, ciSup_const, ↓reduceDIte, le_top, iff_true] exact refl_mem_decompositionGroup K L · have hne0 : ¬ ⨆ x : vL.v.integer, vL.v (s x - x) = 0 := by rw [iSup_val_map_sub_eq_zero_iff_eq_refl hs']; exact hrefl constructor · intro ⟨_, hs⟩ - simp only [hne0, ↓reduceDite, ge_iff_le] + simp only [hne0, ↓reduceDIte, ge_iff_le] rw [show (n : ℕ∞) + 1 = (n + 1 : ℕ) by rfl, ← ENat.some_eq_coe, WithTop.coe_le_coe, Int.le_toNat (by simp only [Left.nonneg_neg_iff, toAdd_iSup_val_map_sub_le_zero_of_ne_zero hs']), le_neg] @@ -349,7 +351,7 @@ theorem mem_lowerRamificationGroup_iff_of_generator exact hs x.1 x.2 · intro h simp only [hs', true_and] - simp only [hne0, ↓reduceDite] at h + simp only [hne0, ↓reduceDIte] at h rw [show (n : ℕ∞) + 1 = (n + 1 : ℕ) by rfl, ← ENat.some_eq_coe, WithTop.coe_le_coe, Int.le_toNat (by simp only [Left.nonneg_neg_iff, toAdd_iSup_val_map_sub_le_zero_of_ne_zero hs']), le_neg] at h @@ -447,7 +449,7 @@ section algebra_instances /-- 1. The conditions might be too strong. 2. The proof is almost the SAME with `Valuation.mem_integer_of_mem_integral_closure`. -/ -instance instIsIntegrallyClosedToValuationSubring : IsIntegrallyClosed 𝒪[K] := by +instance : IsIntegrallyClosed 𝒪[K] := by rw [isIntegrallyClosed_iff K] intro x ⟨p, hp⟩ by_cases xne0 : x = 0 @@ -476,7 +478,7 @@ instance : IsScalarTower 𝒪[K] 𝒪[L] L := inferInstanceAs (IsScalarTower vK. instance [CompleteSpace K] : Algebra.IsIntegral 𝒪[K] 𝒪[L] where isIntegral := by intro ⟨x, hx⟩ - rw [show 𝒪[L] = valuationSubring vL.v by rfl, + rw [show x ∈ 𝒪[L] ↔ x ∈ vL.v.valuationSubring by rfl, (Valuation.isEquiv_iff_valuationSubring _ _).mp (extension_valuation_equiv_extendedValuation_of_discrete (IsValExtension.val_isEquiv_comap (R := K) (A := L))), ← ValuationSubring.mem_toSubring, ← Extension.integralClosure_eq_integer, Subalgebra.mem_toSubring] at hx @@ -491,20 +493,28 @@ instance [CompleteSpace K] : Algebra.IsIntegral 𝒪[K] 𝒪[L] where simp only [ValuationSubring.algebraMap_def] congr -instance [CompleteSpace K] : IsIntegralClosure 𝒪[L] 𝒪[K] L := by - apply IsIntegralClosure.of_isIntegrallyClosed 𝒪[L] 𝒪[K] L +instance [CompleteSpace K] : IsIntegralClosure 𝒪[L] 𝒪[K] L := + IsIntegralClosure.of_isIntegrallyClosed 𝒪[L] 𝒪[K] L + +instance : DiscreteValuationRing 𝒪[K] := by + rw [show 𝒪[K] = vK.v.valuationSubring.toSubring by rfl] + infer_instance + +theorem aux6 [CompleteSpace K] : DiscreteValuationRing 𝒪[L] := + valuationSubring_DVR_of_equiv_discrete + (extension_valuation_equiv_extendedValuation_of_discrete + (IsValExtension.val_isEquiv_comap (R := K) (A := L))) -/-- Can't be inferred within 20000 heartbeats. -/ -instance : IsNoetherianRing 𝒪[K] := PrincipalIdealRing.isNoetherianRing -instance [CompleteSpace K] [IsSeparable K L] : IsNoetherian 𝒪[K] 𝒪[L] := +instance [CompleteSpace K] [Algebra.IsSeparable K L] : IsNoetherian 𝒪[K] 𝒪[L] := IsIntegralClosure.isNoetherian 𝒪[K] K L 𝒪[L] -noncomputable def PowerBasisValExtension [CompleteSpace K] [IsSeparable K L] [IsSeparable (LocalRing.ResidueField 𝒪[K]) (LocalRing.ResidueField 𝒪[L])] : PowerBasis 𝒪[K] 𝒪[L] := +noncomputable def PowerBasisValExtension [CompleteSpace K] [Algebra.IsSeparable K L] [Algebra.IsSeparable (LocalRing.ResidueField 𝒪[K]) (LocalRing.ResidueField 𝒪[L])] : PowerBasis 𝒪[K] 𝒪[L] := letI : Nontrivial vL.v := nontrivial_of_valExtension K L + letI : DiscreteValuationRing 𝒪[L] := aux6 K L PowerBasisExtDVR (integerAlgebra_injective K L) -example [CompleteSpace K] [IsSeparable K L] : +example [CompleteSpace K] [Algebra.IsSeparable K L] : Algebra.FiniteType 𝒪[K] 𝒪[L] := inferInstance end algebra_instances @@ -575,9 +585,9 @@ theorem lowerIndex_of_powerBasis (pb : PowerBasis 𝒪[K] 𝒪[L]) (s : L ≃ₐ i_[L/K] s = if h : s = .refl then (⊤ : ℕ∞) else (- Multiplicative.toAdd (WithZero.unzero (AlgEquiv.val_map_powerBasis_sub_ne_zero pb h))).toNat := by by_cases h : s = .refl - · simp only [h, lowerIndex_refl, ↓reduceDite] + · simp only [h, lowerIndex_refl, ↓reduceDIte] · unfold AlgEquiv.lowerIndex - simp only [h, AlgEquiv.iSup_val_map_sub_eq_powerBasis pb, AlgEquiv.val_map_powerBasis_sub_ne_zero pb h, ↓reduceDite] + simp only [h, AlgEquiv.iSup_val_map_sub_eq_powerBasis pb, AlgEquiv.val_map_powerBasis_sub_ne_zero pb h, ↓reduceDIte] theorem lowerIndex_ne_refl {s : L ≃ₐ[K] L} (hs : s ≠ .refl) : i_[L/K] s ≠ ⊤ := by apply lowerIndex_ne_one @@ -602,7 +612,7 @@ theorem iSup_ne_refl_lowerIndex_ne_top [Nontrivial (L ≃ₐ[K] L)] : rw [← ENat.some_eq_coe, WithTop.coe_untop] simp only [ne_eq, this, Nat.cast_le, ha] -theorem aux0 [IsSeparable K L] [IsSeparable (LocalRing.ResidueField 𝒪[K]) (LocalRing.ResidueField 𝒪[L])] +theorem aux0 [Algebra.IsSeparable K L] [Algebra.IsSeparable (LocalRing.ResidueField 𝒪[K]) (LocalRing.ResidueField 𝒪[L])] {n : ℕ} (hu : n > ⨆ s : {s : (L ≃ₐ[K] L) // s ≠ .refl}, i_[L/K] s) {s : L ≃ₐ[K] L} (hs : s ∈ G(L/K)_[n]) : s = .refl := by apply (mem_lowerRamificationGroup_iff_of_generator (PowerBasis.adjoin_gen_eq_top (PowerBasisValExtension K L)) s.mem_decompositionGroup n).mp at hs @@ -615,8 +625,8 @@ theorem aux0 [IsSeparable K L] [IsSeparable (LocalRing.ResidueField 𝒪[K]) (Lo apply lt_asymm hs this -- this uses local fields and bichang's work, check if the condition is too strong..., It should be O_L is finitely generated over O_K -theorem exist_lowerRamificationGroup_eq_bot [CompleteSpace K] [IsSeparable K L] - [IsSeparable (LocalRing.ResidueField 𝒪[K]) (LocalRing.ResidueField 𝒪[L])] : +theorem exist_lowerRamificationGroup_eq_bot [CompleteSpace K] [Algebra.IsSeparable K L] + [Algebra.IsSeparable (LocalRing.ResidueField 𝒪[K]) (LocalRing.ResidueField 𝒪[L])] : ∃ u : ℤ, G(L/K)_[u] = ⊥ := by by_cases h : Nontrivial (L ≃ₐ[K] L) · use (WithTop.untop _ (iSup_ne_refl_lowerIndex_ne_top K L) : ℕ) + 1 @@ -637,7 +647,7 @@ theorem exist_lowerRamificationGroup_eq_bot [CompleteSpace K] [IsSeparable K L] letI : Subsingleton (L ≃ₐ[K] L) := not_nontrivial_iff_subsingleton.mp h apply Subsingleton.allEq -variable [LocalField K] [LocalField L] [IsSeparable K L] +variable [LocalField K] [LocalField L] [Algebra.IsSeparable K L] end eq_bot diff --git a/RamificationGroup/Unused/Basic.lean b/RamificationGroup/Unused/Basic.lean deleted file mode 100644 index e512649..0000000 --- a/RamificationGroup/Unused/Basic.lean +++ /dev/null @@ -1,64 +0,0 @@ -import Mathlib.Topology.Algebra.Valuation -import Mathlib.RingTheory.DiscreteValuationRing.Basic -import Mathlib.FieldTheory.Galois -import Mathlib.Algebra.Order.Group.TypeTags -import Mathlib.Algebra.Order.Hom.Ring -import LocalClassFieldTheory.DiscreteValuationRing.Extensions - -open DiscreteValuation Valuation - --- this is the same as `[Valued R ℤₘ₀]` `[IsDiscrete hv.v]` use Maria's --- class DiscretelyValued (R : Type*) [Ring R] extends Valued R ℤₘ₀ where --- v_is_surj : (v.toFun).Surjective - -instance {R : Type*} {Γ : outParam Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ] [vR : Valued R Γ]: Preorder R := Preorder.lift vR.v - -structure ValRingHom (R S : Type*) {ΓR ΓS : outParam Type*} [Ring R] [Ring S] - [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓS] - [vR : Valued R ΓR] [vS : Valued S ΓS] extends OrderRingHom R S, ContinuousMap R S where - val_isEquiv_comap' : vR.v.IsEquiv (vS.v.comap toOrderRingHom.toRingHom) - -class ValAlgebra (R A : Type*) {ΓR ΓA : outParam Type*} [CommRing R] [Ring A] [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] [vR : Valued R ΓR] [vA : Valued A ΓA] extends ValRingHom R A, Algebra R A - -variable {K L : Type*} [Field K] [Field L] [vK : Valued K ℤₘ₀] [IsDiscrete vK.v] [CompleteSpace K] [a : Algebra K L] [FiniteDimensional K L] - -#check DiscreteValuation.Extension.valued --- #synth Valued L ℤₘ₀ --- noncomputable instance : Valued L ℤₘ₀ := DiscreteValuation.Extension.valued K L --- this is a def and not an instance because K cannot be infered - -variable [vL : Valued L ℤₘ₀] [IsDiscrete vL.v] - -instance : ValAlgebra K L where -- this uses the uniquess of extension of valuation - toFun := _ - map_one' := _ - map_mul' := _ - map_zero' := _ - map_add' := _ - monotone' := sorry - continuous_toFun := sorry - val_isEquiv_comap' := sorry - smul := a.smul - commutes' := a.commutes' - smul_def' := a.smul_def' - - -variable (K' : IntermediateField K L) [IsGalois K L] - -#synth IsScalarTower K K' L - -instance intermediateField.valued : Valued K' ℤₘ₀ := sorry -- should be scalar tower .valued? -instance : IsDiscrete (intermediateField.valued K').v := sorry -#synth ValAlgebra K K' -#synth ValAlgebra K' L - -instance : ValAlgebra K K' := sorry -instance : ValAlgebra K' L := sorry --- `instance IsValScalarTower K K' L` - - - - -open DiscreteValuation - -#synth LinearOrderedCommGroupWithZero ℤₘ₀ diff --git a/RamificationGroup/Unused/Definition/CompleteValuationRing.lean b/RamificationGroup/Unused/Definition/CompleteValuationRing.lean deleted file mode 100644 index 7e81fcd..0000000 --- a/RamificationGroup/Unused/Definition/CompleteValuationRing.lean +++ /dev/null @@ -1,32 +0,0 @@ -import RamificationGroup.Unused.Definition.MissingPiecesOfMathlib -import Mathlib.RingTheory.Valuation.ValuationSubring -/-! -# Complete Valuation Ring and Complete Discrete Valuation Ring - -In this file, we define --/ - - - -open Classical Uniformity Topology Filter Set -open ValuationRingTopology --- noncomputable --- section - --- variable (R : Type*) [CommRing R] [IsDomain R] [ValuationRing R] - -class CompleteValuationRing (R : Type*) [CommRing R] [IsDomain R] extends ValuationRing R, CompleteSpace R, OrderTopology R --- Note that this definition automatically ensures the topology is induced by valuation by `OrderTopology` and instances of `Order R`, `Topology R` from `ValuationRing R` - ---`Maybe not so bad, A CDVF can be defined as the valued field whose valuation ring is a CDVR` -class CompleteDiscreteValuationRing (R : Type*) [CommRing R] [IsDomain R] extends DiscreteValuationRing R, CompleteValuationRing R - --- Or `ValuedField?` --- Now I believe that the valuation structure on a field is not canonical, so its better to store information of the valuation ring. --- use `mathcal{O}`? -class CompleteValuedField (K : Type*) [Field K] where - O : ValuationSubring K - valuation_subring_is_complete : CompleteValuationRing O - -class CompleteDiscreteValuedField (K : Type*) [Field K] extends CompleteValuedField K where - valuation_subring_is_dvr : DiscreteValuationRing O diff --git a/RamificationGroup/Unused/Definition/ExtensionOfValuation.lean b/RamificationGroup/Unused/Definition/ExtensionOfValuation.lean deleted file mode 100644 index 47e6681..0000000 --- a/RamificationGroup/Unused/Definition/ExtensionOfValuation.lean +++ /dev/null @@ -1,78 +0,0 @@ -import RamificationGroup.Unused.Definition.CompleteValuationRing -import Mathlib.RingTheory.Valuation.Basic - -section - -variable {R₁ R₂ : Type*} [CommRing R₁] [CommRing R₂] {Γ₁ Γ₂ : Type*} [LinearOrderedCommGroupWithZero Γ₁] [LinearOrderedCommGroupWithZero Γ₂] [Algebra R₁ R₂] (v₁ : Valuation R₁ Γ₁) (v₂ : Valuation R₂ Γ₂) - -def RingHom.liftValuationInteger (s : R₁ →+* R₂) (h : v₁.IsEquiv (v₂.comap s)) : 𝒪[v₁] →+* 𝒪[v₂] := sorry - -def PreserveValuation {R₁ R₂} [CommRing R₁] [CommRing R₂] {Γ₁ Γ₂} [LinearOrderedCommMonoidWithZero Γ₁] [LinearOrderedCommMonoidWithZero Γ₂] (v₁ : Valuation R₁ Γ₁) (v₂ : Valuation R₂ Γ₂) (s : R₁ →+* R₂) : Prop := v₁.IsEquiv (v₂.comap s) - -end - --- there are many many usage of Group should be Monoid in mathlib -class ValuationExtension {R₁ R₂} [CommRing R₁] [CommRing R₂] {Γ₁ Γ₂} [LinearOrderedCommMonoidWithZero Γ₁] [LinearOrderedCommMonoidWithZero Γ₂] [Algebra R₁ R₂] (v₁ : Valuation R₁ Γ₁) (v₂ : Valuation R₂ Γ₂) where - val_map : Γ₁ →*₀o Γ₂ - val_extn : ∀ x : R₁, v₂ ((algebraMap R₁ R₂) x) = val_map (v₁ x) - --- I prefer this later definition -class ValuationExtension' {R₁ R₂} [CommRing R₁] [CommRing R₂] {Γ₁ Γ₂} [LinearOrderedCommMonoidWithZero Γ₁] [LinearOrderedCommMonoidWithZero Γ₂] [Algebra R₁ R₂] (v₁ : Valuation R₁ Γ₁) (v₂ : Valuation R₂ Γ₂) where - val_extn : PreserveValuation v₁ v₂ (algebraMap _ _) - - -instance Algebra.liftValuationInteger {R₁ R₂ : Type*} [CommRing R₁] [CommRing R₂] {Γ₁ Γ₂ : Type*} [LinearOrderedCommGroupWithZero Γ₁] [LinearOrderedCommGroupWithZero Γ₂] [Algebra R₁ R₂] (v₁ : Valuation R₁ Γ₁) (v₂ : Valuation R₂ Γ₂) [ValuationExtension v₁ v₂] : Algebra 𝒪[v₁] 𝒪[v₂] := sorry - --- variable {R₁ R₂ : Type*} [CommRing R₁] [CommRing R₂] {Γ₁ Γ₂ : Type*} [LinearOrderedCommGroupWithZero Γ₁] [LinearOrderedCommGroupWithZero Γ₂] [Algebra R₁ R₂] (v₁ : Valuation R₁ Γ₁) (v₂ : Valuation R₂ Γ₂) [ValuationExtension v₁ v₂] --- #synth Algebra 𝒪[v₁] (𝒪[v₂]⧸(𝓂[v₂]^2)) - - --- when R₁ R₂ are field -instance {R₁ R₂ : Type*} [Field R₁] [Field R₂] {Γ₁ Γ₂ : Type*} [LinearOrderedCommGroupWithZero Γ₁] [LinearOrderedCommGroupWithZero Γ₂] [Algebra R₁ R₂] (v₁ : Valuation R₁ Γ₁) (v₂ : Valuation R₂ Γ₂) [ValuationExtension v₁ v₂]: Algebra 𝓀[v₁] 𝓀[v₂] := sorry - - - - - - - --- `def of EquivToDiscrete` - --- `finite extension of (equiv to) discerete valuation is still (equiv to) discrete` - - --- def of EquivToTrivial - --- finite ext of trivial val is still trivial? - - --- `Valuation on any field is either trivial or supp = 0` - - --- `key theorem: If L/K is a finite field extension + more conditions, then any 2 extension of valuations from K on L are equivalent` -theorem Valuation.isEquiv_of_finiteDimensional_of_valuationExtension {K L : Type*} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] {Γ Γ₁ Γ₂ : Type*} [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Γ₁] -[LinearOrderedCommGroupWithZero Γ₂] -(v : Valuation K Γ) (v₁ : Valuation L Γ₁) (v₂ : Valuation L Γ₂) [ValuationExtension v v₁] [ValuationExtension v v₂] : v₁.IsEquiv v₂ := sorry - --- need more conditions -variable {K L : Type*} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] {ΓK ΓL: Type*} [LinearOrderedCommGroupWithZero ΓK] [LinearOrderedCommGroupWithZero ΓL] (vK : Valuation K ΓK) (vL : Valuation L ΓL) [ValuationExtension vK vL] - -theorem Valuation.preserveValuation_of_finiteDimensional_algebra_hom (s : L →ₐ[K] L) : PreserveValuation vL vL s := sorry --- vL.IsEquiv (vL.comap s) := sorry --- (s : L ≃ₐ[K] L) - -def AlgHom.liftValuationInteger (s : L →ₐ[K] L) : 𝒪[vL] →ₐ[𝒪[vK]] 𝒪[vL] := sorry - -def AlgEquiv.liftValuationInteger (s : L ≃ₐ[K] L) : 𝒪[vL] ≃ₐ[𝒪[vK]] 𝒪[vL] := sorry - --- `If preserve valuation is a class, this AlgHom.liftValuationInteger should be make into a Coe instance` - ---def AlgHom.liftValuationIntegerQuotientleIdeal (s : L →ₐ[K] L) (γ : ΓL) : 𝒪[vL]⧸(vL.leIdeal γ) →ₐ[𝒪[vK]] 𝒪[vL]⧸(vL.leIdeal γ) := sorry - ---def AlgEquiv.liftValuationIntegerQuotientleIdeal (s : L ≃ₐ[K] L) (γ : ΓL) : (𝒪[vL]⧸(vL.leIdeal γ)) ≃ₐ[𝒪[vK]] (𝒪[vL]⧸(vL.leIdeal γ)) := sorry - --- `LT version` - -def AlgHom.liftResidueField (s : L →ₐ[K] L) : 𝓀[vL] →ₐ[𝓀[vK]] 𝓀[vL] := sorry - -def AlgEquiv.liftResidueField (s : L ≃ₐ[K] L) : 𝓀[vL] ≃ₐ[𝓀[vK]] 𝓀[vL] := sorry diff --git a/RamificationGroup/Unused/Definition/Herbrand.lean b/RamificationGroup/Unused/Definition/Herbrand.lean deleted file mode 100644 index 8a14d67..0000000 --- a/RamificationGroup/Unused/Definition/Herbrand.lean +++ /dev/null @@ -1,58 +0,0 @@ -import RamificationGroup.Unused.Definition.LowerNumbering -import Mathlib.MeasureTheory.Integral.IntervalIntegral -import RamificationGroup.Unused.MissingPiecesOfMathlib -import Mathlib.GroupTheory.Index -import Mathlib.Logic.Function.Basic -import Mathlib.MeasureTheory.Measure.MeasureSpaceDef -import Mathlib.Algebra.BigOperators.Basic - ---definition of varphi and psi - -open DiscreteValuation Subgroup Set Function MeasureTheory Finset BigOperators - -variable {K L : Type*} [Field K] [Field L] [Algebra K L] (vK : Valuation K ℤₘ₀) (vL : Valuation L ℤₘ₀) [ValuationExtension vK vL] -variable {μ : Measure ℝ} -variable (vK : Valuation K ℤₘ₀) (vL : Valuation L ℤₘ₀) [ValuationExtension vK vL] - -noncomputable def Index_of_G_i (u : ℚ) : ℚ := - if u > 0 then - relindex' G(vL/vK)_[0] G(vL/vK)_[(Int.ceil u)] - else - relindex' G(vL/vK)_[0] G(vL/vK)_[(Int.floor u)] - -noncomputable def varphi' (u : ℚ) : ℚ := - 1 / (Index_of_G_i vK vL u) - -noncomputable def varphi (u : ℚ) : ℚ := - if u ≥ 1 then - ∑ x in Finset.Icc 0 (Int.floor u), (varphi' vK vL x) + (u - (Int.floor u)) * (varphi' vK vL u) - else if u < 1 ∧ 0 ≤ u then - u * (varphi' vK vL u) - else - (-u) * (varphi' vK vL u) - -noncomputable def psi : ℚ → ℚ := - invFun (varphi vK vL) - -theorem varphi_zero_eq_zero : varphi vK vL 0 = 0 := by - unfold varphi - simp - -theorem varphi_negone_eq_negone : varphi vK vL -1 = -1 := by - unfold varphi varphi' - sorry - -noncomputable def psi' (v : ℚ): ℚ := - 1 / (varphi' vK vL (psi vK vL v)) - -theorem psi_zero_eq_zero : psi vK vL 0 = 0 := by - unfold psi - simp only [invFun] - - -theorem varphi_bij : Function.Bijective (varphi vK vL) := by sorry - -theorem psi_bij : Function.Bijective (psi vK vL) := by sorry - ---lemma 3 -theorem Varphi_eq_Sum_Inf (u : ℚ) : (varphi vK vL u) = (1 / Nat.card G(vL/vK)_[0]) * (∑ x in (Finset G(vL/vK)_[(Int.ceil u)]) , min (u + 1) ((i[vL/vK] x)))- 1 := by sorry diff --git a/RamificationGroup/Unused/Definition/LowerNumbering.lean b/RamificationGroup/Unused/Definition/LowerNumbering.lean deleted file mode 100644 index 97b8762..0000000 --- a/RamificationGroup/Unused/Definition/LowerNumbering.lean +++ /dev/null @@ -1,124 +0,0 @@ -import RamificationGroup.Unused.Definition.ExtensionOfValuation -import Mathlib.Algebra.Group.WithOne.Defs -import Mathlib.FieldTheory.Galois - - --- rename this file to RamificationFiltration or something - --- `Mathlib.RingTheory.Ideal.QuotientOperations` --- def AlgHom.QuotientLift {R S₁ S₂ : Type*} [CommRing R] [CommRing S₁] [CommRing S₂] [Algebra R S₁] [Algebra R S₂] {I : Ideal R} {J₁ : Ideal S₁} {J₂ : Ideal S₂} (h₁ : I ≤ J₁.comap (algebraMap R S₁)) (h₂ : I ≤ J₂.comap (algebraMap R S₂)) : S₁⧸J₁ →ₐ[R⧸I] S₂⧸J₂ := sorry - -open DiscreteValuation - -section --- An alternative thought on definition of ValuationExtension - - --- Maybe use `Valued` here is far better, Valued K + Finite K L will automatically create some ValuationExtension K L, However, this need to rewrite the definition of ValuationExtension - -class ValuationExtension'' (K L : Type*) [Field K] [Field L] {ΓK: outParam (Type*)} {ΓL : outParam (Type*)} [LinearOrderedCommGroupWithZero ΓK] [LinearOrderedCommGroupWithZero ΓL] [Valued K ΓK] [Valued L ΓL] where - toAlgebra : Algebra K L - val_extn : PreserveValuation Valued.v Valued.v (algebraMap K L) - -variable {K L : Type*} [Field K] [Field L] [Algebra K L] [Valued K ℤₘ₀] [Valued L ℤₘ₀] -#check ValuationExtension'' K L - --- And there is Valued instance on K L! --- Maybe ValuationExtension is not a good name... - -notation:max K:max " →ᵥ " L:max => ValuationExtension'' K L --- or "→+*ᵥ" - --- divide into 2 parts, ` →ᵥ ` and `ValuedAlgebra`, first is the set of all possible maps preserving valuation, second is when there is a canonical map - -instance : Coe (ValuationExtension'' K L) (Algebra K L) := - ⟨fun f => f.toAlgebra⟩ - -instance : CoeFun (ValuationExtension'' K L) (fun _ => K → L) := sorry - -variable (f : K →ᵥ L) (k : K) -#check f k - --- ValuedScalarTower, automated infered from other instances -end - -section - -variable {K L : Type*} [Field K] [Field L] [Algebra K L] (vK : Valuation K ℤₘ₀) (vL : Valuation L ℤₘ₀) [ValuationExtension vK vL] --some more condition to make sure vL(pi) = 1, probably uniformizer, same as Maria's definition - -def Valuation.ramificationIndex (vK : Valuation K ℤₘ₀) (vL : Valuation L ℤₘ₀) [ValuationExtension vK vL] : ℤ := sorry -- Or it is possible to use other people's definition, here just a theorem relate its relation with valuation of the uniformizer - -notation:max " e(" vL:max "/" vK:max ") " => Valuation.ramificationIndex vK vL - -#check 𝓂[vL] - --- `theorem TFAE` --- fix O / m^i --- ∀ a : 𝒪[vL], vL ( a - s a) >= i --- generator x, vL(x - sx) >= i - -instance: Coe ℤ (Multiplicative ℤ) := ⟨fun x => x⟩ - -variable {G : Type*} [Group G] - -#synth CoeTC G (WithZero G) -instance : Coe ℤ ℤₘ₀ := ⟨fun x => ((x : Multiplicative ℤ): WithZero ℤ) ⟩ - -def DiscreteValuation.toInt (i : ℤₘ₀) : WithTop ℤ := sorry -variable (i : ℤₘ₀) -#check toInt i - --- a general instance? for well founded orders -instance : InfSet (WithTop ℤ) := sorry - -def lowerIndex (s : L ≃ₐ[K] L) : WithTop ℤ := iInf (fun x : 𝒪[vL] => toInt (vL (s.liftValuationInteger vK vL x - x))) -1 - -def RamificationGroup (i : ℤ) : Subgroup (L ≃ₐ[K] L) where - carrier := --{s : L ≃ₐ[K] L | ∀ x : 𝒪[vL], toInt (vL (s.liftValuationInteger vK vL x - x)) ≥ i + 1 } - {s : L ≃ₐ[K] L | lowerIndex vK vL s ≥ i} - mul_mem' := sorry - one_mem' := sorry - inv_mem' := sorry - -notation:max " i[" vL:max "/" vK:max "]" => lowerIndex vK vL - -notation:max " G(" vL:max "/" vK:max ")_[" n:max "] " => RamificationGroup vK vL n - - -#check i[vL/vK] -#check G(vL/vK)_[1] - - - --- Many properties --- `i <=1, = ⊤` `the filtration is complete` - --- currently there is no subgroup filtration, only ideal filtration, maybe to define it is useful. --- `the filtration is decreasing, and seperable` - -end - -section - -variable {K L : Type*} [Field K] [Field L] [Algebra K L] (K' : IntermediateField K L) [IsGalois K L] (vK : Valuation K ℤₘ₀) (vK' : Valuation K' ℤₘ₀) (vL : Valuation L ℤₘ₀) [ValuationExtension vK vL] [ValuationExtension vK' vL] --some more condition - --- `key theorem : lower numbering is compatible with subgroup` restate this into a better form... -theorem lower_numbering_inf (i : ℤ) : ((G(vL/vK)_[i]).subgroupOf K'.fixingSubgroup ).map (IntermediateField.fixingSubgroupEquiv K') = G(vL/vK')_[i] := sorry - -theorem index_subgroup (s : K'.fixingSubgroup) : i[vL/vK'] (K'.fixingSubgroupEquiv s) = i[vL/vK] s := sorry - - -variable [Normal K K'] [ValuationExtension vK vK'] --this should be later changed in to a scalar-tower-like instance -variable [FiniteDimensional K L] -#synth FiniteDimensional K K' -#synth Finite (L ≃ₐ[K] L) -#synth Finite (K' ≃ₐ[K] K') - -open BigOperators - --- need instances of computation rules related to WithTop ℤ -instance : Coe (WithTop ℤ) (WithTop ℚ) := sorry -#synth Mul (WithTop ℚ) -theorem index_quotient_group (s₀ : L ≃ₐ[K] L) : i[vK'/vK] (s₀.restrictNormal K') = ((1 / e(vL/vK) :ℚ) : (WithTop ℚ)) * ∑ s in {s : L ≃ₐ[K] L | s.restrictNormal K' = s₀.restrictNormal K'}.toFinite.toFinset, i[vL/vK] s := sorry --- do we need to def this index finset separately? -end diff --git a/RamificationGroup/Unused/Definition/MissingPiecesOfMathlib.lean b/RamificationGroup/Unused/Definition/MissingPiecesOfMathlib.lean deleted file mode 100644 index 89ecdaf..0000000 --- a/RamificationGroup/Unused/Definition/MissingPiecesOfMathlib.lean +++ /dev/null @@ -1,117 +0,0 @@ -import Mathlib.RingTheory.Valuation.ValuationRing -import Mathlib.RingTheory.DiscreteValuationRing.Basic -import Mathlib.Topology.UniformSpace.Cauchy -import Mathlib.Topology.Algebra.Ring.Basic -import Mathlib.Topology.Order.Basic -import Mathlib.Topology.Algebra.Valuation -import Mathlib.Algebra.Order.Hom.Monoid -import Mathlib.Algebra.Order.Group.TypeTags -import Mathlib.GroupTheory.Index - -/-! -# Missing Pieces of Mathlib - -In this file, we collect missing theorems, instances as prequisite of this project. Theorems in this file should be added to mathlib file scatterly into each file. --/ -set_option autoImplicit false - -section ValuationTopology -variable (R: Type*) --- variable {Γ₀ : Type*} [LinearOrderedCommMonoidWithZero Γ₀] - -namespace ValuationRingTopology -variable [CommRing R] [IsDomain R] [ValuationRing R] - -/-- The preorder of divisibility associated to a valuation ring, i.e. `a ≤ b` if there exist `c`, such that `a * c = b`. -/ -scoped instance : Preorder R where - le a b := ∃ c, a * c = b - le_refl _ := ⟨1, mul_one _⟩ - le_trans _ _ _ := fun ⟨u, h⟩ ⟨v, g⟩ => ⟨u * v, by rw [← g, ← h]; ring⟩ - --- /-- The topology on a valuation ring `R` is defined to be the topology associated to the preorder of divisibility.-/ --- scoped instance : TopologicalSpace R := Preorder.topology R - --- scoped instance : OrderTopology R := ⟨rfl⟩ - --- scoped instance : UniformSpace R where --- uniformity := sorry --- refl := sorry --- symm := sorry --- comp := sorry --- isOpen_uniformity := sorry - - -/-! --- the following is missed in `Mathlib.RingTheory.Valuation.ValuationRing` - -def ValuationRing.setoid : Setoid R where - r a b := a ≤ b ∧ b ≤ a - -- 2 elements is equiv if both a ≤ b and b ≤ a - iseqv := sorry - - -def ValuationRing.ValueMonoid := Quotient (ValuationRing.setoid R) -- this is really a monoid with zero - -instance : LinearOrderedCommMonoidWithZero (ValuationRing.ValueMonoid R) := sorry - -scoped instance : Valued R (ValuationRing.ValueMonoid R) := _ - --- `Valued` uses Group instead of Monoid... `Maybe the correct way is to generalize mathlib's valued to monoid instead of group???` --/ - -scoped instance : Valued R (ValuationRing.ValueGroup R (FractionRing R)) := sorry - -scoped instance : OrderTopology R where - topology_eq_generate_intervals := sorry - --- the topology not rfl to -scoped instance : TopologicalRing R := sorry - - -section ValuationIdeal - - - --- Mathlib.RingTheory.Valuation.Integers -def Valuation.leIdeal {R : Type*} {Γ₀ : Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (γ : Γ₀) : Ideal (Valuation.integer v) := sorry --- when gamma < 1, the ideal is whole ring - -def Valuation.ltIdeal {R : Type*} {Γ₀ : Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (γ : Γ₀) : Ideal (Valuation.integer v) := sorry --- when gamma < 1, the ideal is whole ring - -def Valuation.maximalIdeal {R : Type*} {Γ₀ : Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) : Ideal (Valuation.integer v) := Valuation.ltIdeal v 1 -- def use either localring.maximalideal or v < 1, then show the remaining one as theorem when K is a field - -notation:max " 𝒪[" v:max "] " => Valuation.integer v - -notation:max " 𝓂[" v:max "] " => Valuation.maximalIdeal v - -variable {R : Type*} {Γ₀ : Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) -#check 𝒪[v] --- `In Discrete Valuation Ring, relation between LT LE Ideal` - -variable {R : Type*} {Γ₀ : Type*} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) - --- Need field -instance : (Valuation.maximalIdeal v).IsMaximal := sorry - -end ValuationIdeal - -section ValuationInteger -variable {K L : Type*} [Field K] [Field L] {ΓK ΓL : Type*} [LinearOrderedCommGroupWithZero ΓK][LinearOrderedCommGroupWithZero ΓL] [Algebra K L] {vK : Valuation K ΓK} {vL : Valuation L ΓL} - -instance : ValuationRing vK.integer where - cond' := sorry - --- `the maximal ideal = the lt ideal` - -notation:max " 𝓀[" v:max "] " => LocalRing.ResidueField ↥𝒪[v] - -#check 𝓀[vK] --- `instance, when 𝓀[vK] is a field` - - --- `Key theorem, OL/OK is generated by 1 element` - -end ValuationInteger - --- `Instance of trivial group Unit being LinearOrderedCommGroupWithZero diff --git a/RamificationGroup/Unused/Discrete.lean b/RamificationGroup/Unused/Discrete.lean deleted file mode 100644 index edcdc24..0000000 --- a/RamificationGroup/Unused/Discrete.lean +++ /dev/null @@ -1,64 +0,0 @@ -import RamificationGroup.Valued.Defs -import Mathlib.FieldTheory.Galois - -open DiscreteValuation Valuation - -section - --- `key def : If L/K a finite field extension of local field, then there exist a extension of valuation`, see Maria and Phillip, `discrete_valuation_ring.extensions` - -def DiscretelyValued.extensionFiniteDimension {K} (L) [Field K] [Field L] [vK : Valued K ℤₘ₀] [IsDiscrete vK.v] [Algebra K L] [FiniteDimensional K L] : Valued L ℤₘ₀ := sorry - --- instance : Valued L - --- `key theorem: If L/K is a finite field extension + more conditions, then any 2 extension of valuations from K on L are equivalent`; Discrete Valuations are equal -theorem Valuation.isEquiv_of_finiteDimensional {K L : Type*} [Field K] [Field L] {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] [vK : Valued K ℤₘ₀] [IsDiscrete vK.v] [vL : Valued L Γ] [ValAlgebra K L] [FiniteDimensional K L] - : vL.v.IsEquiv (vK.extensionFiniteDimension L).v := sorry --- DiscreteValuation.Extension.integralClosure_eq_integer see Maria - -variable {K L : Type*} [Field K] [Field L] [vK : Valued K ℤₘ₀] [IsDiscrete vK.v] [a : Algebra K L] [FiniteDimensional K L] - - -instance : DiscretelyValued L := sorry -- see Maria and Phillip - -instance : ValAlgebra K L where - toFun := _ - map_one' := _ - map_mul' := _ - map_zero' := _ - map_add' := _ - monotone' := sorry - continuous_toFun := sorry - val_isEquiv_comap' := sorry - smul := a.smul - commutes' := a.commutes' - smul_def' := a.smul_def' - - -variable (K' : IntermediateField K L) [IsGalois K L] - --- should instances of Discretely Valued L, K' auto generated from K? also [ValAlgebra K L] -instance : ValAlgebra K K' := sorry -instance : ValAlgebra K' L := sorry --- `instance IsValScalarTower K K' L` - - - - - - --- any alg map preserves valuation, thus we can define a function input alg map output val alg map - - --- some Unique instance? - - --- Unique instance in the case of Local Fields, which comes from uniqueness of extension of valuation. - - --- `Canonical Isom between AlgEquiv and ValAlgEquiv!` -variable {K L : Type*} [Field K] [Field L] {Γ : Type*} [vK : DiscretelyValued K] [vL : DiscretelyValued L] [ValAlgebra K L] [FiniteDimensional K L] - -def AlgEquiv.toValAlgEquiv : (L ≃ₐ[K] L) ≃* (L ≃ₐv[K] L) := sorry - -end diff --git a/RamificationGroup/Unused/DiscreteValuation.lean b/RamificationGroup/Unused/DiscreteValuation.lean deleted file mode 100644 index fbf1392..0000000 --- a/RamificationGroup/Unused/DiscreteValuation.lean +++ /dev/null @@ -1,39 +0,0 @@ -import Mathlib.RingTheory.Valuation.Basic -import Mathlib.Algebra.Order.WithZero -import Mathlib.Algebra.Order.Group.TypeTags - -namespace DiscreteValuation - -section examples --- #synth Coe ℤ (WithTop ℤ) -#synth CoeTC ℤ (WithTop ℤ) - -#check ((-1 : ℤ) : WithTop ℤ) - --- #synth Coe ℤ (Multiplicative ℤ) - -#check Multiplicative.ofAdd -#check Multiplicative.toAdd - - -example : ℤₘ₀ := .coe (.ofAdd (2 : ℤ)) --- the order is the same with Z, 0 is bottom element -example : (.coe (.ofAdd (2 : ℤ)) : ℤₘ₀) ≥ .coe (.ofAdd (1 : ℤ)) := by decide - -example : (.coe (.ofAdd (3 : ℤ)) : ℤₘ₀) ≥ 0 := by decide - -#check (⊥ : ℤₘ₀) -example : 0 = (⊥ : ℤₘ₀) := by rfl - -end examples - -def ofInt : ℤ →o ℤₘ₀ where - toFun := .coe - monotone' _ _ := WithZero.coe_le_coe.mpr -example : ℤₘ₀ := .coe $ .ofAdd $ -3 -#check (.coe 1 : ℤₘ₀) -scoped instance : Coe ℤ ℤₘ₀ where - coe := ofInt - --- lots of simp lemmas, related to ofInt, try to copy from `Mathlib.Algebra.Order.Monoid.WithZero.Defs` (WithZero) and `Mathlib.Algebra.Group.TypeTags` (Multiplicative) -end DiscreteValuation diff --git a/RamificationGroup/Unused/Integer.lean b/RamificationGroup/Unused/Integer.lean deleted file mode 100644 index 315e015..0000000 --- a/RamificationGroup/Unused/Integer.lean +++ /dev/null @@ -1,53 +0,0 @@ -import Mathlib.RingTheory.Valuation.Integers -import RamificationGroup.Preliminary.DiscreteValuation - -#check Valuation.integer -#check Valuation.ltAddSubgroup -- `Make use of this!!` - --- Mathlib.RingTheory.Valuation.Integers -def Valuation.leIdeal {R : Type*} {Γ₀ : outParam Type*} [Ring R] - [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (γ : Γ₀) : Ideal (v.integer) where - carrier := {x : v.integer | v x ≤ γ} - add_mem' ha hb := .trans (v.map_add_le_max' _ _) (max_le ha hb) - zero_mem' := by - show v 0 ≤ γ - simp only [map_zero, zero_le'] - smul_mem' c a ha := by - show v (c * a) ≤ γ - calc - _ = v c * v a := v.map_mul' _ _ - _ ≤ 1 * γ := mul_le_mul' c.2 ha - _ = γ := one_mul _ - -theorem Valuation.leIdeal_eq_top {R : Type*} {Γ₀ : outParam Type*} [Ring R] - [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) {γ : Γ₀} (h : 1 ≤ γ) : v.leIdeal γ = ⊤ := sorry --- when gamma ≥ 1, the ideal is whole ring - --- special value when γ = 0 -def Valuation.ltIdeal {R : Type*} {Γ₀ : outParam Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (γ : Γ₀) : Ideal (Valuation.integer v) := if h : γ = 0 then ⊥ else { - carrier := {x : v.integer | v x < γ}, - add_mem' := fun ha hb ↦ lt_of_le_of_lt (v.map_add_le_max' _ _) (max_lt ha hb), - zero_mem' := by - show v 0 < γ - simpa only [map_zero, zero_lt_iff], - smul_mem' := fun c a ha ↦ by - show v (c * a) < γ - calc - _ = v c * v a := v.map_mul' _ _ - _ ≤ 1 * v a := mul_le_mul' c.2 (le_refl _) - _ = v a := one_mul _ - _ < γ := ha - } - -theorem Valuation.ltIdeal_eq_top {R : Type*} {Γ₀ : outParam Type*} [Ring R] - [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) {γ : Γ₀} (h : 1 < γ) : v.ltIdeal γ = ⊤ := sorry --- when gamma < 1, the ideal is whole ring - --- inclusion relation,... - -namespace DiscreteValuation --- `In Discrete Valuation Ring, relation between LT LE Ideal` - -theorem leIdeal_eq_ltIdeal_add_one {R : Type*} [Ring R] (v : Valuation R ℤₘ₀) (n : ℤ) : v.leIdeal (ofInt n) = v.ltIdeal (ofInt (n + 1)) := sorry - -end DiscreteValuation diff --git a/RamificationGroup/Unused/MissingPiecesOfMathlib.lean b/RamificationGroup/Unused/MissingPiecesOfMathlib.lean deleted file mode 100644 index 1671f29..0000000 --- a/RamificationGroup/Unused/MissingPiecesOfMathlib.lean +++ /dev/null @@ -1,99 +0,0 @@ -import Mathlib.RingTheory.Valuation.ValuationRing -import Mathlib.RingTheory.DiscreteValuationRing.Basic -import Mathlib.Topology.UniformSpace.Cauchy -import Mathlib.Topology.Algebra.Ring.Basic -import Mathlib.Topology.Order.Basic -import Mathlib.Topology.Algebra.Valuation -import Mathlib.Data.Real.Basic -/-! -# Missing Pieces of Mathlib - -In this file, we collect missing theorems, instances as prequisite of this project. Theorems in this file should be added to mathlib file scatterly into each file. --/ - -variable (R: Type*) --- variable {Γ₀ : Type*} [LinearOrderedCommMonoidWithZero Γ₀] - -namespace ValuationTopology -variable [CommRing R] [IsDomain R] [ValuationRing R] - -/-- The preorder of divisibility associated to a valuation ring, i.e. `a ≤ b` if there exist `c`, such that `a * c = b`. -/ -scoped instance : Preorder R where - le a b := ∃ c, a * c = b - le_refl _ := ⟨1, mul_one _⟩ - le_trans _ _ _ := fun ⟨u, h⟩ ⟨v, g⟩ => ⟨u * v, by rw [← g, ← h]; ring⟩ - -/-- The topology on a valuation ring `R` is defined to be the topology associated to the preorder of divisibility.-/ -scoped instance : TopologicalSpace R := Preorder.topology R - -scoped instance : OrderTopology R := ⟨rfl⟩ - -scoped instance : UniformSpace R where - uniformity := sorry - refl := sorry - symm := sorry - comp := sorry - isOpen_uniformity := sorry - - -/-! --- the following is missed in `Mathlib.RingTheory.Valuation.ValuationRing` - -def ValuationRing.setoid : Setoid R where - r a b := a ≤ b ∧ b ≤ a - -- 2 elements is equiv if both a ≤ b and b ≤ a - iseqv := sorry - - -def ValuationRing.ValueMonoid := Quotient (ValuationRing.setoid R) -- this is really a monoid with zero - -instance : LinearOrderedCommMonoidWithZero (ValuationRing.ValueMonoid R) := sorry - -scoped instance : Valued R (ValuationRing.ValueMonoid R) := _ - --- `Valued` uses Group instead of Monoid... `Maybe the correct way is to generalize mathlib's valued to monoid instead of group???` --/ - - -end ValuationTopology - - - -section OrderHom - ---class OrderMonoidHom (A B : Type*) [Preorder A] [Preorder B] [MulOneClass A] [MulOneClass B] extends OrderHom A B, MonoidHom A B - -infix : 50 " →*o " => OrderMonoidHom - -#check MonoidWithZeroHom - ---class OrderMonoidWithZeroHom (A B : Type*) [Preorder A] [Preorder B] [MulZeroOneClass A] [MulZeroOneClass B] extends OrderHom A B, MonoidWithZeroHom A B - -variable {A B : Type*} [LinearOrderedCommMonoidWithZero A] [LinearOrderedCommMonoidWithZero B] -#check OrderMonoidWithZeroHom A B - -end OrderHom - - -/- -class CompleteDiscreteValuationRing (R : Type*) [CommRing R] [IsDomain R] extends CompleteValuationRing R where - is_discrete : sorry - --- Maybe these two definition is not so necessary -class CompleteValuationField (R : Type*) [Field R] extends CompleteValuationRing R - -class CompleteDiscreteValuationField (R : Type*) [Field R] extends CompleteValuationRing R --/ - - - - -open Subgroup -section - -variable {G : Type*} [Group G] (H L K : Subgroup G) - -noncomputable def relindex' : ℚ := - (K.index : ℚ) / (H.index: ℚ) - -end diff --git a/RamificationGroup/Unused/RamificationIndex.lean b/RamificationGroup/Unused/RamificationIndex.lean deleted file mode 100644 index 7aaac51..0000000 --- a/RamificationGroup/Unused/RamificationIndex.lean +++ /dev/null @@ -1,31 +0,0 @@ -import RamificationGroup.Valued.Defs -import RamificationGroup.Valued.Hom.Basic -import RamificationGroup.Valued.Hom.Discrete -import RamificationGroup.LowerNumbering - -open DiscreteValuation Valuation Valued - -namespace ValRingHom - -variable {R S : Type*} {ΓR ΓS : outParam Type*} [Ring R] [Ring S] [DiscretelyValued R] [DiscretelyValued S] - -def ramificationIndex {R S : Type*} {ΓR ΓS : outParam Type*} [Ring R] [Ring S] [DiscretelyValued R] [DiscretelyValued S] (f : ValRingHom R S) : ℕ := sorry -- min of .v (image of elements of R that has val > 1 in S) --- `ℕ, not WithTop ℕ` - -variable {K K' L : Type*} {ΓK ΓK' : outParam Type*} [CommRing K] [Field K'] [Field L] [LinearOrderedCommGroupWithZero ΓK] -[LinearOrderedCommGroupWithZero ΓK'] [vL : Valued L ℤₘ₀] [Algebra K L] -[Algebra K K'] [Algebra K' L] [IsScalarTower K K' L] - -/-- `h` should be `𝒪[L] is finite over 𝒪[K]`-/ -theorem lowerIndex_ne_refl_of_FG (h : sorry) {s : L ≃ₐ[K] L} (hs : s ≠ .refl) : i_[L/K] s ≠ ⊤ := by - intro heq - simp only [AlgEquiv.lowerIndex, AddSubgroupClass.coe_sub, - dite_eq_left_iff, ENat.coe_ne_top, imp_false, not_not] at heq - have : ∀ x : vL.v.integer, v (s x - x) = 0 := sorry - apply hs; ext x - rw [AlgEquiv.coe_refl, id_eq, ← sub_eq_zero, ← Valuation.zero_iff vL.v] - rcases ValuationSubring.mem_or_inv_mem 𝒪[L] x with h | h - sorry; sorry - - --- properties of ramification index, multiplicativity diff --git a/RamificationGroup/Unused/Test.lean b/RamificationGroup/Unused/Test.lean deleted file mode 100644 index 198c158..0000000 --- a/RamificationGroup/Unused/Test.lean +++ /dev/null @@ -1,93 +0,0 @@ -import Mathlib.RingTheory.DiscreteValuationRing.Basic -import Mathlib.Topology.Algebra.Valuation -import Mathlib.Algebra.Order.WithZero -import Mathlib.Algebra.Order.Group.TypeTags -import Mathlib.FieldTheory.Galois -import LocalClassFieldTheory.LocalField -import Mathlib.NumberTheory.NumberField.Basic -import Mathlib.Analysis.Normed.Group.Basic -import Mathlib.RingTheory.DedekindDomain.Ideal - -open Classical multiplicity - - -open DiscreteValuation - - - -#check Ideal.uniqueFactorizationMonoid - - - -/-- `multiplicity a b` returns the largest natural number `n` such that - `a ^ n ∣ b`, as a `PartENat` or natural with infinity. If `∀ n, a ^ n ∣ b`, - then it returns `⊤`-/ -def multiplicity' [Monoid α] [DecidableRel ((· ∣ ·) : α → α → Prop)] (a b : α) : PartENat := - PartENat.find fun n => ¬a ^ (n + 1) ∣ b - -theorem finite_nat_iff' {a b : ℕ} : Finite a b ↔ a ≠ 1 ∧ 0 < b := by sorry --- rw [← not_iff_not, not_finite_iff_forall, not_and_or, Ne.def, Classical.not_not, not_lt, --- le_zero_iff] --- exact --- ⟨fun h => --- or_iff_not_imp_right.2 fun hb => --- have ha : a ≠ 0 := fun ha => hb <| zero_dvd_iff.mp <| by rw [ha] at h; exact h 1 --- Classical.by_contradiction fun ha1 : a ≠ 1 => --- have ha_gt_one : 1 < a := --- lt_of_not_ge fun _ => --- match a with --- | 0 => ha rfl --- | 1 => ha1 rfl --- | b+2 => by linarith --- not_lt_of_ge (le_of_dvd (Nat.pos_of_ne_zero hb) (h b)) (lt_pow_self ha_gt_one b), --- fun h => by cases h <;> simp [*]⟩ --- #align multiplicity.finite_nat_iff multiplicity.finite_nat_iff - -/-- For `p ≠ 1`, the `p`-adic valuation of a natural `n ≠ 0` is the largest natural number `k` such -that `p^k` divides `z`. If `n = 0` or `p = 1`, then `padicValNat p q` defaults to `0`. -/ -def padicValNat' (p : ℕ) (n : ℕ) : ℕ := - if h : p ≠ 1 ∧ 0 < n then (multiplicity p n).get (multiplicity.finite_nat_iff.2 h) else 0 - - -theorem finite_ideal_iff {A : Type u_2} [CommRing A] [IsDomain A] [IsDedekindDomain A] - {p : Ideal A} [Ideal.IsMaximal p] {a : A} : - multiplicity.Finite p (Ideal.span {a}) ↔ a ≠ 0:= sorry - - -noncomputable abbrev ord {K : Type _} [Field K] [NumberField K] - (p : Ideal (NumberField.ringOfIntegers K)) - [Ideal.IsMaximal p] (x : (NumberField.ringOfIntegers K)) : PartENat := - (multiplicity p (Ideal.span {x})) - --- variable {K : Type _} [Field K] [NumberField K] (p : Ideal (NumberField.ringOfIntegers K)) --- #synth IsDedekindDomain (NumberField.ringOfIntegers K) - -theorem ord_top {K : Type _} [Field K] [NumberField K] - {p : Ideal (NumberField.ringOfIntegers K)} - [Ideal.IsMaximal p] {x : (NumberField.ringOfIntegers K)} - : ord p x ≠ ⊤ → x ≠ 0 := sorry - -noncomputable def exp_ord {K : Type _} [Field K] [NumberField K] - (p : Ideal (NumberField.ringOfIntegers K)) - [Ideal.IsMaximal p] (x : (NumberField.ringOfIntegers K)) : NNReal := - if h : ord p x = ⊤ then 0 else (1/2) ^ ((ord p x).get (finite_ideal_iff.mpr (ord_top h))) - - --- DiscreteValuation.termℤₘ₀ (open discretevaluation) - - -namespace DiscreteValuation - -variable {K L : Type*} [Field K] [vK : Valued K ℤₘ₀] [Field L] [Algebra K L] [IsDiscrete vK.v] [CompleteSpace K] {K' : IntermediateField K L} [FiniteDimensional K K'] - -instance valuedIntermediateField : Valued K' ℤₘ₀ := DiscreteValuation.Extension.valued K K' - -/- -- success -#synth IsDiscrete (valuedIntermediateField.v : Valuation K' _) --/ - --- this is needed, or #synth CompleteSpace K' fails --- `when is this needed?` -instance (priority := 100) : CompleteSpace K' := DiscreteValuation.Extension.completeSpace K K' - -end DiscreteValuation diff --git a/RamificationGroup/Unused/Trash/draft.lean b/RamificationGroup/Unused/Trash/draft.lean deleted file mode 100644 index 91a1dd2..0000000 --- a/RamificationGroup/Unused/Trash/draft.lean +++ /dev/null @@ -1,38 +0,0 @@ -import Mathlib.LinearAlgebra.Dimension.Finrank -import Mathlib.RingTheory.IntegralClosure -import Mathlib.RingTheory.DiscreteValuationRing.Basic -import Mathlib.RingTheory.DedekindDomain.AdicValuation -import Mathlib.RingTheory.Polynomial.Eisenstein.Basic -import Mathlib.Data.Polynomial.Basic -import Mathlib.RingTheory.DedekindDomain.AdicValuation -import Mathlib.RingTheory.DedekindDomain.Ideal -import Mathlib.RingTheory.Ideal.Operations -import Mathlib.LinearAlgebra.Matrix.Charpoly.Basic -import Mathlib.LinearAlgebra.Matrix.Basis -import Mathlib.LinearAlgebra.FreeModule.Basic -import Mathlib.LinearAlgebra.Charpoly.Basic -import Mathlib.Algebra.Algebra.Tower -import Mathlib.Algebra.Algebra.Basic -import Mathlib.FieldTheory.Galois -import RamificationGroup.Unused.Definition.LowerNumbering - -section - -open Polynomial RingHom IsDedekindDomain FiniteDimensional DiscreteValuationRing Ideal Algebra - -variable {A : Type*} [CommRing A] [IsDomain A] [DiscreteValuationRing A] -variable {p : Ideal A} -variable {K : Type*} [Field K] [Algebra A K] [IsFractionRing A K] -variable {L : Type*} [Field L] [Algebra K L] [Module.Finite K L] [Algebra A L] [IsScalarTower A K L] -variable {B : Type*} [CommRing B] [Algebra B L] [Algebra A B] [Algebra K B] [IsIntegralClosure B A L] - [IsDomain B] [DiscreteValuationRing B] [SMulCommClass B K L] [IsScalarTower A B L] -(va : HeightOneSpectrum A) (vb : HeightOneSpectrum B) -[HMul PartENat ℕ PartENat] - -variable {a : A} - -theorem Prop18 {x : B} (h0 : Irreducible x) (h1 : ∀ a : A, (addVal A a) * (finrank K L) = addVal B (algebraMap A B a)) : -(ker (aeval x)) = (Ideal.span {LinearMap.charpoly (lsmul A K L x)}) := by sorry - - -def aaa (f : ℕ → ℕ) := ∀ x y, f (x + y) = f x + f y ∧ ∀ x c, f (c * x) = c * f x diff --git a/RamificationGroup/Unused/Trash/old - SubAlgEquiv.lean b/RamificationGroup/Unused/Trash/old - SubAlgEquiv.lean deleted file mode 100644 index 11bfff6..0000000 --- a/RamificationGroup/Unused/Trash/old - SubAlgEquiv.lean +++ /dev/null @@ -1,21 +0,0 @@ -/- -GOAL : construct `S ≃ₐ B` for `S = ⊤ : Subalgebra A B` - -might not be good to use `LinearEquiv.ofTop` - --/ - -import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed - -variable {A : Type _} {B : Type _} [CommSemiring A] [Semiring B] [Algebra A B] -variable {S : Subalgebra A B} (hS : S = ⊤) -variable {x : B} (hx : Algebra.adjoin A {x} = ⊤) - -def LinearEquiv.ofSubalgebraEqTop : S ≃ₗ[A] B := - LinearEquiv.ofTop (Subalgebra.toSubmodule S) (Algebra.toSubmodule_eq_top.mpr hS) - -def AlgEquiv.ofTop : S ≃ₐ[A] B := by - apply AlgEquiv.ofLinearEquiv (LinearEquiv.ofSubalgebraEqTop hS) - · unfold LinearEquiv.ofSubalgebraEqTop - sorry - · sorry diff --git a/RamificationGroup/Unused/Trash/old-Herbrand.lean b/RamificationGroup/Unused/Trash/old-Herbrand.lean deleted file mode 100644 index c1b826f..0000000 --- a/RamificationGroup/Unused/Trash/old-Herbrand.lean +++ /dev/null @@ -1,856 +0,0 @@ -import RamificationGroup.LowerNumbering -import Mathlib.MeasureTheory.Integral.IntervalIntegral -import Mathlib.GroupTheory.Index -import Mathlib.Logic.Function.Basic -import Mathlib.MeasureTheory.Measure.MeasureSpaceDef -import Mathlib.Algebra.BigOperators.Basic - -open DiscreteValuation Subgroup Set Function MeasureTheory Finset BigOperators Int Valued Eq -open DiscreteValuation Subgroup Set Function Finset BigOperators Int Valued - -namespace HerbrandFunction - -section - -variable {G : Type*} [Group G] (H L K : Subgroup G) --- `can be changed to use relindex` -noncomputable def _root_.Subgroup.relindex' : ℚ := - (K.index : ℚ) / (H.index: ℚ) -theorem ceil_nonpos {u : ℚ} (h : u ≤ 0) : ⌈u⌉ ≤ 0 := by - by_contra h - push_neg at * - have : ¬u ≤ 0 := by linarith [ceil_pos.1 h] - contradiction - -end -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] - --- 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]) - --- scoped notation:max " φ_[" L:max "/" K:max "]" => phi K L - -noncomputable def Index_of_G_i (u : ℚ) : ℚ := - if u > (-1) then - relindex G(S/R)_[0] G(S/R)_[(Int.ceil u)] - else - 1 -noncomputable def phi (u : ℚ) : ℚ := - ∑ x in Finset.Icc 1 (⌈u⌉ - 1), (phiDeriv R S x) + (u - (max 0 (⌈u⌉ - 1))) * (phiDeriv R S u) - -noncomputable def phiDeriv (u : ℚ) : ℚ := - 1 / (Index_of_G_i R S u) - -noncomputable def phi (u : ℚ) : ℚ := - if u ≥ 1 then - ∑ x in Finset.Icc 1 (Int.floor u), (phiDeriv R S x) + (u - (Int.floor u)) * (phiDeriv R S u) - else - u * (phiDeriv R S u) - ---for mathlib -theorem sub_of_sum (a : ℤ) (f : ℚ → ℚ) (h : 1 ≤ a): ∑ x in Icc 1 (a + 1), f x - ∑ x in Icc 1 a, f x = f (a + 1) := by - have hncons : (a + 1) ∉ Finset.Icc 1 a := by simp - have hcons : (Finset.Icc 1 (a + 1)) = cons (a + 1) (Finset.Icc 1 a) hncons := by - ext n - simpa using (by omega) - rw [hcons] - rw [sum_cons] -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 - ---for mathlib -theorem ceil_eq_floor_add_one_iff (u : ℚ) (h : u ≠ ⌊u⌋) : ⌈u⌉ = ⌊u⌋ + 1 := by - have hu : fract u ≠ 0 := by - unfold fract - by_contra h' - have : u = ⌊u⌋ := by linarith [h'] - contradiction - have h' : ⌈u⌉ = u + 1 - Int.fract u := by - apply ceil_eq_add_one_sub_fract hu - unfold fract at h' - have h'': (⌈u⌉ : ℚ) = ((⌊u⌋ + 1) : ℚ):= by - rw [h'] - ring - exact_mod_cast h'' - ---for mathlib -theorem Int.eq_of_ge_of_lt_add_one (a m : ℤ) (h1 : m ≤ a) (h2 : a < (m + 1)) : a = m := by - have hle : a ≤ m + 1 - 1 := by apply le_sub_one_iff.2 h2 - simp at hle - apply ((LE.le.ge_iff_eq h1).1 hle).symm - -theorem phiDeriv_eq_ceil (u : ℚ) : phiDeriv R S u = phiDeriv R S ⌈u⌉ := by - unfold phiDeriv Index_of_G_i - by_cases h : -1 < u - · have hcl : ⌈u⌉ > (-1 : ℚ) := by - apply lt_of_lt_of_le - apply h - apply le_ceil - simp [h, hcl] - have hcl : ¬⌈u⌉ > (-1 : ℚ) := by - by_contra hc - have hcl' : -1 < ⌈u⌉ := by apply cast_lt.1 hc - have : -1 < u := by - apply lt_ceil.1 hcl' - contradiction - simp [h, hcl] -theorem phi_eq_self_of_le_zero {u : ℚ} (hu : u ≤ 0) : phi R S u = u := by - unfold phi - simp [phiDeriv_eq_one_of_le_zero R S hu] - have h : ⌈u⌉ - 1 ≤ 0 := by linarith [ceil_nonpos hu] - have h' : ⌈u⌉ - 1 < 1 := by linarith [h] - calc - _ = (u - max 0 (⌈u⌉ - 1)) := by simp [h'] - _ = u := by simp [h] - -theorem phiDeriv_pos (u : ℚ) : 0 < phiDeriv R S u := by - unfold phiDeriv Index_of_G_i relindex index - by_cases h : u > -1 - simp [h] - sorry - sorry - -- apply div_pos_iff.2 - -- left - -- constructor <;> sorry - -- simp [h] - -theorem phiDeriv_neg_int_eq_one {u : ℤ} (hu : u ≤ 0) : phiDeriv R S u = 1 := by - unfold phiDeriv Index_of_G_i - by_cases hgt : (-1 : ℚ) < u - · simp [hgt] - have hzero : 0 = u := by - have hgt' : -1 < u := by apply cast_lt.1 hgt - have hge : -1 ≤ u - 1 := by - apply le_sub_one_iff.2 hgt' - simp at hge - apply (LE.le.ge_iff_eq hge).1 hu - have hzero' : u = (0 : ℚ) := by simp [hzero] - sorry - simp [hgt] - 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.2 ⟨sorry, sorry⟩ - exact_mod_cast h - -theorem phi_int_succ (a : ℤ) : (phi R S a) = (phi R S (a + 1)) - (phiDeriv R S (a + 1)) := by - unfold phi - by_cases hgeone : (1 : ℚ) ≤ a - · have hgezero : (0 : ℚ) ≤ a := by linarith - simp [hgeone, hgezero] - have h : ∑ x in Icc 1 (a + 1), phiDeriv R S ↑x = phiDeriv R S (a + 1) + ∑ x in Icc 1 a, phiDeriv R S ↑x := by - have hgeone' : 1 ≤ a := by apply cast_le.1 hgeone - have h' : ∑ x in Finset.Icc 1 (a + 1), phiDeriv R S ↑x - ∑ x in Finset.Icc 1 a, phiDeriv R S ↑x = phiDeriv R S (↑a + 1) := by - apply sub_of_sum a (phiDeriv R S) hgeone' - linarith [h'] - simp [h] - by_cases hgezero : (0 : ℚ) ≤ a - · have heqzero : (0 : ℚ) = a := by - --this - push_neg at hgeone - have hgeone' : a < 1 := by - apply cast_lt.1 hgeone - have hlezero : a ≤ (0 : ℚ) := by - convert le_sub_one_iff.2 hgeone' - simp - apply (LE.le.ge_iff_eq hgezero).1 hlezero - erw [←heqzero] - simp [hgeone, hgezero] - simp [hgeone, hgezero] - push_neg at * - ring_nf - apply mul_eq_mul_left_iff.2 - left - rw [phiDeriv_neg_int_eq_one] - have : (1 + a) ≤ 0 := by - have hgezero' : a < 0 := by apply cast_lt.1 hgezero - have hle: a ≤ 0 - 1 := by - convert le_sub_one_iff.2 hgezero' - linarith [hle] - symm - convert phiDeriv_neg_int_eq_one R S this -theorem phiDeriv_eq_ceil {u : ℚ} : phiDeriv R S u = phiDeriv R S ⌈u⌉ := by - unfold phiDeriv - simp - apply le_of_lt - apply cast_lt.1 hgezero - -theorem phi_eq_self_of_le_neg_one {u : ℚ} (hu : u ≤ 0) : phi R S u = u := by - unfold phi phiDeriv Index_of_G_i relindex - have hu' : ¬u ≥ 1 := by linarith [hu] - simp [hu'] - by_cases hu' : -1 < u - <;> simp [hu'] - · have hu'' : ⌈u⌉ = 0 := by - apply ceil_eq_iff.2 - constructor - simp [hu']; simp [hu] - sorry - -theorem phi_mono_int {a1 a2 : ℤ} (h : a1 < a2) : (phi R S a1) < (phi R S a2) := by - have hsub : a2 = a1 + (a2 - a1 - 1) + 1 := by ring - rw [hsub] - induction' a2 - a1 - 1 with n ih - · induction' n with n ih - · apply sub_lt_zero.1 - rw [phi_int_succ R S a1] - simp - apply phiDeriv_pos - apply lt_trans - apply ih - simp - apply sub_lt_zero.1 - have heq : phi R S (↑a1 + ↑n + 1) = phi R S (↑a1 + (↑n + 1) + 1) - (phiDeriv R S (a1 + n + 1 + 1)) := by - convert phi_int_succ R S (a1 + n + 1) - <;>simp - ring - rw [heq] - simp - apply phiDeriv_pos - sorry - -theorem phi_mono_int' (a1 a2 : ℤ) (h : a1 ≤ a2) : (phi R S a1) ≤ (phi R S a2) := by - by_cases heq : a1 = a2 - simp [heq] - apply le_of_lt - push_neg at * - have hlt : a1 < a2 := by apply lt_of_le_of_ne h heq - apply phi_mono_int R S hlt - ---i'll change this name -theorem phi_rational_floor (a : ℚ) : (phi R S a) = (phi R S ⌊a⌋) + ((phi R S (⌊a⌋ + 1)) - (phi R S ⌊a⌋)) * (a - ⌊a⌋) := by - by_cases ha : a ≥ 1 - · unfold phi - have hfl : (1 : ℚ) ≤ ⌊a⌋ := by - convert le_floor.2 ha - simp - apply cast_le - have hfl' : (0 : ℚ) ≤ ⌊a⌋ := by - linarith [hfl] - simp [ha, hfl, hfl'] - nth_rw 2 [mul_comm] - apply mul_eq_mul_left_iff.2 - by_cases hzero : fract a = 0 - · right - exact hzero - left - have h : ∑ x in Finset.Icc 1 (⌊a⌋ + 1), phiDeriv R S ↑x - ∑ x in Finset.Icc 1 ⌊a⌋, phiDeriv R S ↑x = phiDeriv R S (⌊a⌋ + 1) := by - have hfl' : (1 : ℤ) ≤ ⌊a⌋ := by apply cast_le.1 hfl - apply sub_of_sum ⌊a⌋ (phiDeriv R S) hfl' - rw [h, phiDeriv_eq_ceil] - have hflcl : ⌈a⌉ = ⌊a⌋ + 1 := by - unfold fract at hzero - push_neg at hzero - have : a ≠ ⌊a⌋ := by - by_contra hc - have hc' : a - ⌊a⌋ = 0 := by linarith - contradiction - apply ceil_eq_floor_add_one_iff a this - rw [hflcl] - congr - simp - have hfl : ¬ (1 : ℚ) ≤ ↑⌊a⌋ := by - by_contra h' - have h'' : (1 : ℚ) ≤ a := by - apply le_floor.1 - convert h' - simp - apply cast_le.symm - contradiction - by_cases hzero : (0 : ℚ) ≤ ⌊a⌋ - · unfold phi - simp [ha, hfl, hzero] - push_neg at * - --and this is the same - have hflzero : 0 = ⌊a⌋ := by - have hfl' : ⌊a⌋ < 1 := by apply cast_lt.1 hfl - have hlezero : ⌊a⌋ ≤ 1 - 1 := by - apply le_sub_one_iff.2 hfl' - simp at hlezero - have hgezero : 0 ≤ ⌊a⌋ := by apply cast_le.1 hzero - apply (LE.le.ge_iff_eq hgezero).1 hlezero - unfold fract - simp [hflzero.symm] - rw [mul_comm] - apply mul_eq_mul_right_iff.2 - by_cases hzero' : a = 0 - · right - exact hzero' - left - have hcl : ⌈a⌉ = 1 := by - have hgtzero : (0 : ℚ) < a := by - apply lt_of_le_of_ne - have : ⌊a⌋ ≤ a := by apply floor_le - apply le_trans - apply hzero - apply this - push_neg at hzero' - apply hzero'.symm - apply ceil_eq_on_Ioc - simp - constructor - apply hgtzero - apply le_of_lt ha - rw [phiDeriv_eq_ceil, hcl] - congr - simp [ha, hfl, hzero] - push_neg at * - have ha' : a < 0 := by sorry - rw [phi_eq_self_of_le_neg_one R S (by linarith [ha']), phi_eq_self_of_le_neg_one R S (by linarith [hzero])] -theorem phi_pos_of_pos {u : ℚ} (hu : 0 < u) : 0 < phi R S u := by - unfold phi - have hzero' : ⌊a⌋ + 1 < 1 := by sorry - have hzero'' : ¬0 ≤ ⌊a⌋ := by sorry - simp [hzero', hzero''] - unfold fract - sorry - have h : 0 ≤ ∑ x in Finset.Icc 1 (⌈u⌉ - 1), phiDeriv R S x := by - --apply sum_pos - sorry - have h' : 0 < (u - (max 0 (⌈u⌉ - 1))) * phiDeriv R S u := by - apply mul_pos - simp [hu] - linarith [ceil_lt_add_one u] - exact phiDeriv_pos R S u - linarith [h, h'] - -theorem phi_pos_gt_nonpos {a b : ℚ} (hu1 : a ≤ 0) (hu2 : 0 < b) : phi R S a < phi R S b := by - apply lt_of_le_of_lt (b := 0) - rw [phi_eq_self_of_le_zero] - <;> exact hu1 - exact phi_pos_of_pos R S hu2 - -theorem phi_of_pos_of_le_one {u : ℚ} (h1 : 0 < u) (h2 : u ≤ 1) : phi R S u = u * phiDeriv R S u := by - unfold phi - have huc : ⌈u⌉ = 1 := by - apply ceil_eq_iff.2 - simp [h1, h2] - have huf1 : ⌈u⌉ - 1 < 1 := by linarith [huc] - have huf0 : ⌈u⌉ - 1 = 0 := by simp [huc] - simp [huf1, huf0] - -#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 phi_rational_ceil (a : ℚ) : (phi R S a) = (phi R S (⌊a⌋ + 1)) - ((phi R S (⌊a⌋ + 1)) - (phi R S ⌊a⌋)) * (⌊a⌋ - a + 1) := by - by_cases ha : (1 : ℚ) ≤ a - · unfold phi - have hfl : (1 : ℚ) ≤ ⌊a⌋ := by - convert le_floor.2 ha - apply cast_le - have hcl : (1 : ℚ) ≤ (⌊a⌋ + 1) := by - linarith [hfl] - simp [ha, hcl, hfl] - have h : ∑ x in Finset.Icc 1 (⌊a⌋ + 1), phiDeriv R S ↑x - ∑ x in Finset.Icc 1 ⌊a⌋, phiDeriv R S ↑x = phiDeriv R S (⌊a⌋ + 1) := by - have hfl' : (1 : ℤ) ≤ ⌊a⌋ := by apply cast_le.1 hfl - apply sub_of_sum ⌊a⌋ (phiDeriv R S) hfl' - have h' : (∑ x in Finset.Icc 1 (⌊a⌋ + 1), phiDeriv R S ↑x - ∑ x in Finset.Icc 1 ⌊a⌋, phiDeriv R S ↑x) - fract a * phiDeriv R S a - - (∑ x in Finset.Icc 1 (⌊a⌋ + 1), phiDeriv R S ↑x - ∑ x in Finset.Icc 1 ⌊a⌋, phiDeriv R S ↑x) * (↑⌊a⌋ - a + 1) = 0 := by - rw [h] - by_cases hfl' : a - ⌊a⌋ = 0 - · unfold fract - have : ⌊a⌋ - a = 0 := by linarith [hcl] - simp [hcl, this] - left - unfold fract - linarith [this] - push_neg at * - have hcl' : (⌈a⌉ : ℚ) = (⌊a⌋ : ℚ) + 1:= by - have hfl'' : a ≠ ⌊a⌋ := by - by_contra hc - have : a - ⌊a⌋ = 0 := by linarith [hc] - contradiction - have hcl'' : ⌈a⌉ = ⌊a⌋ + 1:= by - apply ceil_eq_floor_add_one_iff a hfl'' -theorem phi_strictMono_of_gt_one {a b : ℚ} (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] - apply (mul_lt_mul_right (by apply phiDeriv_pos R S)).2 - simp [hab] - · calc - _ ≤ ∑ x in Finset.Icc 1 ⌈a⌉, phiDeriv R S x := by - have h : (a - ↑(max 0 (⌈a⌉ - 1))) * phiDeriv R S ⌈a⌉ ≤ 1 * phiDeriv R S ⌈a⌉ := by - apply (mul_le_mul_right (by apply phiDeriv_pos R S)).2 - sorry - apply le_trans (b := ∑x in Finset.Icc 1 (⌈a⌉ - 1), phiDeriv R S ↑x + 1 * phiDeriv R S ⌈a⌉) - rw [phiDeriv_eq_ceil] - linarith [h] - 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 - apply le_of_eq h - _ ≤ ∑ x in Finset.Icc 1 (⌈b⌉ - 1), phiDeriv R S x := by - have h : ⌈a⌉ ≤ ⌈b⌉ - 1 := by - have hc : ⌈a⌉ < ⌈b⌉ := by - apply lt_of_le_of_ne - apply ceil_le_ceil - linarith [hab] - push_neg at hceil - 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 - ring_nf - nth_rw 3 [phiDeriv_eq_ceil] - unfold fract - have heq : phiDeriv R S (1 + ⌊a⌋) = phiDeriv R S ⌈a⌉ := by - rw [hcl'] - have : 1 + (⌊a⌋ : ℚ) = (⌊a⌋ : ℚ) + 1 := by ring - rw [this] - rw [heq] - ring - linarith [h'] - have hfl : ¬(1 : ℚ) ≤ ⌊a⌋ := by - by_contra hc - have hge : (1 : ℚ) ≤ a := by - apply le_floor.1 - convert hc - simp - apply cast_le.symm - contradiction - by_cases hcl : (1 : ℚ) ≤ (⌊a⌋ + 1) - · unfold phi - simp [ha, hcl, hfl] - push_neg at * - have hfl' : ⌊a⌋ = 0 := by - simp at hcl - have hfl' : ⌊a⌋ < 1 := by apply cast_lt.1 hfl - apply Int.eq_of_ge_of_lt_add_one ⌊a⌋ 0 hcl hfl' - simp [hfl'] - by_cases hzero : a = 0 - · simp [hzero] - have h : phiDeriv R S a = phiDeriv R S 1 := by - have h' : phiDeriv R S a = phiDeriv R S ⌈a⌉ := by - apply phiDeriv_eq_ceil - rw [h'] - have hcl' : ⌈a⌉ = (1 : ℚ) := by - have hnefl : a ≠ ⌊a⌋ := by - rw [hfl'] - push_neg at hzero - apply hzero - have : ⌈a⌉ = ⌊a⌋ + 1 := by - apply ceil_eq_floor_add_one_iff a hnefl - rw [this] - simp [hfl'] - rw [hcl'] - ring_nf - simp [h] - push_neg at * - have hcl' : (⌊a⌋ : ℚ) ≤ 0 := by sorry - have ha' : a < 0 := by sorry - simp [phi_eq_self_of_le_neg_one R S (by linarith [ha']), phi_eq_self_of_le_neg_one R S hcl'] - sorry - - -theorem phi_gt_floor : ∀ a : ℚ , (a ≠ ⌊a⌋) → (phi R S a) > (phi R S ⌊a⌋) := by - rintro a ha - apply gt_iff_lt.2 - apply sub_lt_zero.1 - nth_rw 2 [phi_rational_floor] - simp - apply mul_pos_iff.2 - left - constructor - simp - convert phi_mono_int R S (show ⌊a⌋ < ⌊a⌋ + 1 by linarith) - simp - apply fract_pos.2 ha - -theorem phi_lt_ceil : ∀ a : ℚ , (phi R S a) < (phi R S (⌊a⌋ + 1)) := by - rintro a - apply gt_iff_lt.2 - apply sub_lt_zero.1 - nth_rw 1 [phi_rational_ceil] - simp - apply mul_pos_iff.2 - left - constructor - simp - convert phi_mono_int R S (show ⌊a⌋ < ⌊a⌋ + 1 by linarith) - simp - have h : a - 1 < ⌊a⌋ := by apply sub_one_lt_floor - linarith [h] - -theorem phi_mono_in_section : ∀ a1 a2 : ℚ , (⌊a1⌋ = ⌊a2⌋) ∧ (a1 < a2) → (phi R S a1) < (phi R S a2) := by - rintro a1 a2 ⟨h1, h2⟩ - apply gt_iff_lt.2 - apply sub_lt_zero.1 - nth_rw 2 [phi_rational_floor] - nth_rw 1 [phi_rational_floor] - rw [h1] - simp - apply sub_lt_zero.1 - have : ((phi R S (↑⌊a2⌋ + 1)) - (phi R S ↑⌊a2⌋)) * (a1 - ↑⌊a2⌋) - ((phi R S (↑⌊a2⌋ + 1)) - (phi R S ↑⌊a2⌋)) * fract a2 = ((phi R S (↑⌊a2⌋ + 1)) - (phi R S ↑⌊a2⌋)) * (a1 - a2) := by - unfold fract - calc - ((phi R S (↑⌊a2⌋ + 1)) - (phi R S ↑⌊a2⌋)) * (a1 - ↑⌊a2⌋) - ((phi R S (↑⌊a2⌋ + 1)) - (phi R S ↑⌊a2⌋)) * (a2 - ⌊a2⌋) = ((phi R S (↑⌊a2⌋ + 1)) - (phi R S ↑⌊a2⌋)) * ((a1 - ⌊a2⌋) - (a2 - ⌊a2⌋)) := by - ring - _ = ((phi R S (↑⌊a2⌋ + 1)) - (phi R S ↑⌊a2⌋)) * (a1 - a2) := by - --apply sum_le_sum_of_subset h' (f := phiDeriv R S) - _ < phi R S b := by - unfold phi - simp - left - unfold fract - ring - rw [this] - apply mul_neg_iff.2 - left - constructor - simp - convert phi_mono_int R S (show ⌊a2⌋ < ⌊a2⌋ + 1 by linarith) - simp - simp [h2] - ---i'll change this name too -theorem phi_mono_over_section : ∀ a1 a2 : ℚ , (⌊a1⌋ ≠ ⌊a2⌋) ∧ (a1 < a2) → (phi R S a1) < (phi R S a2) := by - rintro a1 a2 ⟨hne, hlt⟩ - by_cases hfloor : a2 = ⌊a2⌋ - have hle : ⌊a1⌋ + 1 ≤ ⌊a2⌋ := by - have hlt : ⌊a1⌋ < ⌊a2⌋ := by - apply lt_of_le_of_ne - apply floor_le_floor - apply le_of_lt hlt - apply hne - apply add_one_le_of_lt hlt - apply lt_of_lt_of_le - have h1 : (phi R S a1) < (phi R S (⌊a1⌋ + 1)) := by apply (phi_lt_ceil R S) - apply h1 - have h2 : (phi R S (⌊a1⌋ + 1)) ≤ (phi R S a2) := by - by_cases heq : (⌊a1⌋ + 1) = a2 - simp [heq] - push_neg at heq - have h1' : (phi R S (⌊a1⌋ + 1)) ≤ (phi R S ⌊a2⌋) := by - convert phi_mono_int' R S (⌊a1⌋ + 1) ⌊a2⌋ hle - simp - rw [hfloor] - exact h1' - apply h2 - have hle : a1 ≤ ⌊a2⌋ := by - by_contra hc - push_neg at * - have h : ⌊a1⌋ = ⌊a2⌋ := by - have h1 : ⌊a1⌋ ≤ ⌊a2⌋ := by - apply floor_le_floor - apply le_of_lt - exact hlt - have h2 : ⌊a2⌋ ≤ ⌊a1⌋ := by - apply le_floor.2 - apply le_of_lt hc - apply (LE.le.ge_iff_eq h1).1 h2 - contradiction - have hlt : ⌊a2⌋ < a2 := by - have hge : ⌊a2⌋ ≤ a2 := by apply floor_le - push_neg at hfloor - apply lt_of_le_of_ne hge hfloor.symm - apply lt_of_le_of_lt - have h1 : (phi R S a1) ≤ (phi R S ⌊a2⌋) := by - by_cases heq : a1 = ⌊a2⌋ - simp [heq] - apply le_of_lt - apply lt_of_lt_of_le - push_neg at * - have hlt' : a1 < ⌊a2⌋ := by apply lt_of_le_of_ne hle heq - have h1' : (phi R S a1) < (phi R S (⌊a1⌋ + 1)) := by apply phi_lt_ceil R S - apply h1' - have hle' : ⌊a1⌋ + 1 ≤ ⌊a2⌋ := by - push_neg at * - have hlt' : ⌊a1⌋ < ⌊a2⌋ := by - have hle'' : ⌊a1⌋ ≤ ⌊a2⌋ := by - apply floor_le_floor - apply le_of_lt - assumption - apply lt_of_le_of_ne hle'' hne - apply Int.le_of_lt_add_one - linarith [hlt'] - have h2' : (phi R S ↑(⌊a1⌋ + 1)) ≤ (phi R S (⌊a2⌋)) := by - apply phi_mono_int' R S (⌊a1⌋ + 1) ⌊a2⌋ hle' - convert h2' - simp - apply h1 - push_neg at hfloor - have h2 : (phi R S ⌊a2⌋) < (phi R S a2) := by apply (phi_gt_floor R S a2 hfloor) - apply h2 - -theorem phi_mono_iff : (∀a1 a2 : ℚ , a1 < a2 → (phi R S a1) < (phi R S a2)) ↔ (∀a1 a2 : ℤ , a1 < a2 → (phi R S a1) < (phi R S a2)) := by - constructor - rintro _ a1 a2 - apply phi_mono_int R S - rintro _ a1 a2 h' - by_cases hfloor : ⌊a1⌋ = ⌊a2⌋ - apply phi_mono_in_section - constructor <;> assumption - push_neg at * - apply phi_mono_over_section - constructor <;> assumption - apply mul_pos - simp - constructor - · linarith [hb] - · linarith [ceil_lt_add_one b] - apply phiDeriv_pos R S - -theorem phi_strictMono : StrictMono (phi R S) := by - rintro a1 a2 - revert a1 a2 - apply (phi_mono_iff R S).2 - apply phi_mono_int - -theorem phi_bij : Function.Bijective (phi R S) := by - constructor - rintro a1 a2 h - contrapose! h - by_cases h1 : a1 > a2 - have hlt : (phi R S a2) < (phi R S a1) := by - apply phi_strictMono - apply h1 - apply ne_of_gt hlt - have hlt : (phi R S a2) > (phi R S a1) := by - apply phi_strictMono - apply lt_of_not_ge - rintro a b h - by_cases ha0 : a ≤ 0 - · by_cases hb0 : b ≤ 0 - · rw [phi_eq_self_of_le_zero R S ha0, phi_eq_self_of_le_zero R S hb0]; assumption - · by_cases hb1 : b ≤ 1 - · push_neg at * - apply phi_pos_gt_nonpos R S ha0 hb0 - · push_neg at * - apply phi_pos_gt_nonpos R S ha0 hb0 - · by_cases ha1 : a ≤ 1 - push_neg at * - exact lt_of_le_of_ne h1 h - apply ne_of_lt hlt - rintro b - unfold phi phiDeriv - by_cases hb : b < 0 - sorry - sorry - have hac : ⌈a⌉ = 1 := by - apply ceil_eq_iff.2 - simp [ha0, ha1] - · by_cases hb1 : b ≤ 1 - · push_neg at * - have hbc : ⌈b⌉ = 1 := by - apply ceil_eq_iff.2 - simp [lt_trans ha0 h, hb1] - have hceil : ⌈a⌉ = ⌈b⌉ := by simp [hac, hbc] - have hderiv : phiDeriv R S a = phiDeriv R S b := by - unfold phiDeriv - simp [hceil] - rw [phi_of_pos_of_le_one R S ha0 ha1, phi_of_pos_of_le_one R S (by linarith) hb1] - simp [hderiv] - 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 - - ---i don't know -theorem exist_aux (y : ℚ) : ∃ n , phi R S (n - 1) ≤ y ∧ y < phi R S n := by sorry - - -theorem phi_Bijective : 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, 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 - - -noncomputable def psi : ℚ → ℚ := - invFun (phi R S) - -theorem psi_bij : Function.Bijective (psi R S) := by - constructor - have hpsi: (invFun (phi R S)).Injective := - (rightInverse_invFun (phi_bij R S).2).injective - (rightInverse_invFun (phi_Bijective R S).2).injective - exact hpsi - apply invFun_surjective - apply (phi_bij R S).1 - apply (phi_Bijective R S).1 - -theorem phi_zero_eq_zero : phi R S 0 = 0 := by - unfold phi - simp - -noncomputable def psi' (v : ℚ): ℚ := - 1 / (phiDeriv R S (psi R S v)) - -theorem psi_zero_eq_zero : psi R S 0 = 0 := by - theorem psi_zero_eq_zero : psi R S 0 = 0 := by - unfold psi - nth_rw 1 [← phi_zero_eq_zero R S] - have : id 0 = (0 : ℚ) := by rfl - nth_rw 2 [← this] - have Inj : (phi R S).Injective := by apply (phi_bij R S).1 - have Inj : (phi R S).Injective := by apply (phi_Bijective R S).1 - rw [← invFun_comp Inj] - simp - -theorem leftInverse_phi_psi : Function.LeftInverse (phi R S) (psi R S) := by - rintro a - apply invFun_eq - apply (phi_bij R S).surjective - apply (phi_Bijective R S).surjective - -@[simp] -theorem phi_psi_eq_self (u : ℚ) : (phi R S) ((psi R S) u) = u := leftInverse_phi_psi R S u - - -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_neg_one R S hv - apply (phi_bij R S).injective - have h2 : phi R S v = v := by apply phi_eq_self_of_le_zero R S hv - apply (phi_Bijective R S).injective - simp [h1, h2] - ---lemma 3 -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] - -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 - -theorem G_pairwiseDisjoint (n : ℤ) : (PairwiseDisjoint (↑(Finset.Icc (-1) (n - 1))) (G_diff K L)) := by - induction' n with n ih - induction' n with n ih - simp - sorry -theorem Ramification_Group_pairwiseDisjoint (n : ℤ) : (PairwiseDisjoint (↑(Finset.Icc (-1) (n - 1))) (Ramification_Group_diff K L)) := by - sorry - ---i don't know how to name them -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 * - sorry - - -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 hc - apply hx'' - apply h - 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 - sorry - -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 G_split (n : ℤ) : (⊤ : Finset (L ≃ₐ[K] L)) = (disjiUnion (Finset.Icc (-1) (n - 1)) (G_diff K L) (G_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 phi_eq_sum_inf (u : ℚ) : (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 h : u ≥ 1 - · simp [h] - have hsplit : (Finset.sum (⊤ : Finset (L ≃ₐ[K] L)) (AlgEquiv.truncatedLowerIndex K L (u + 1) ·)) = (Finset.sum (((disjiUnion (Finset.Icc (-1) (⌈u⌉ - 1)) (G_diff K L) (G_pairwiseDisjoint K L _)))) ((AlgEquiv.truncatedLowerIndex K L (u + 1) ·))) + (Finset.sum (((G(L/K)_[(⌈u⌉)] : Set (L ≃ₐ[K] L)).toFinset)) ((AlgEquiv.truncatedLowerIndex K L (u + 1) ·))) := by - calc - _ = (Finset.sum (((disjiUnion (Finset.Icc (-1) (⌈u⌉ - 1)) (G_diff K L) (G_pairwiseDisjoint K L _)) ∪ (G(L/K)_[(⌈u⌉)] : Set (L ≃ₐ[K] L)).toFinset)) ((AlgEquiv.truncatedLowerIndex K L (u + 1) ·))) := by - congr - apply G_split - _ = (Finset.sum (((disjiUnion (Finset.Icc (-1) (⌈u⌉ - 1)) (G_diff K L) (G_pairwiseDisjoint K L _)))) ((AlgEquiv.truncatedLowerIndex K L (u + 1) ·))) + (Finset.sum (((G(L/K)_[(⌈u⌉)] : Set (L ≃ₐ[K] L)).toFinset)) ((AlgEquiv.truncatedLowerIndex K L (u + 1) ·))) := by - have : Disjoint (disjiUnion (Finset.Icc (-1) (⌈u⌉ - 1)) (G_diff K L) (G_pairwiseDisjoint K L _)) (toFinset ↑ G(L/K)_[⌈u⌉]) := by sorry - apply sum_union - apply this - have hsplit' : (Finset.sum (((disjiUnion (Finset.Icc (-1) (⌈u⌉ - 1)) (G_diff K L) (G_pairwiseDisjoint K L _)))) ((AlgEquiv.truncatedLowerIndex K L (u + 1) ·))) = Finset.sum _ fun (i : ℤ) => Finset.sum _ fun (x : _) => (AlgEquiv.truncatedLowerIndex K L (u + 1) x) := by - apply sum_disjiUnion - simp at hsplit hsplit' - rw [hsplit, hsplit'] - have hu : (Finset.sum ((G(L/K)_[(⌈u⌉)] : Set (L ≃ₐ[K] L)).toFinset) ((AlgEquiv.truncatedLowerIndex K L (u + 1) ·))) = (u + 1) * (Nat.card G(L/K)_[⌈u⌉]) := by - convert Sum_Trunc_lower_Index_of_G_n K L ⌈u⌉ u (by apply le_ceil) - rw [hu] - have hd : Finset.sum (Finset.Icc (-1) (⌈u⌉ - 1)) (fun (i : ℤ) => Finset.sum (G_diff K L i) (fun (x : _) => (AlgEquiv.truncatedLowerIndex K L (u + 1) x))) = Finset.sum (Finset.Icc (-1) (⌈u⌉ - 1)) fun (i : ℤ) => (i + 1) * (Nat.card ((G(L/K)_[i] : Set (L ≃ₐ[K] L)) \ G(L/K)_[(i + 1)] : Set (L ≃ₐ[K] L))):= by - norm_num - apply sum_equiv (.refl ℤ) - simp - simp - rintro i hge hle - have hle' : i ≤ u := by - sorry - convert Sum_Trunc_lower_Index_of_diff_G K L i u hle' - unfold G_diff - simp - sorry - rw [hd] - sorry - unfold phi - simp [h] - sorry - --- scoped notation:max " ψ_[" L:max "/" K:max "]" => psi K L - -end HerbrandFunction diff --git a/RamificationGroup/Unused/Trash/test.lean b/RamificationGroup/Unused/Trash/test.lean deleted file mode 100644 index 80eb29d..0000000 --- a/RamificationGroup/Unused/Trash/test.lean +++ /dev/null @@ -1,199 +0,0 @@ -import RamificationGroup.LowerNumbering -import Mathlib.MeasureTheory.Integral.IntervalIntegral -import RamificationGroup.Unused.MissingPiecesOfMathlib -import Mathlib.GroupTheory.Index -import Mathlib.Logic.Function.Basic -import Mathlib.MeasureTheory.Measure.MeasureSpaceDef -import Mathlib.Algebra.BigOperators.Basic - ---definition of varphi and psi - -open DiscreteValuation Subgroup Set Function MeasureTheory Finset BigOperators - -variable (R S : Type*) {ΓR : outParam Type*} [CommRing R] [Ring S] [LinearOrderedCommGroupWithZero ΓR] [vR : Valued R ΓR] [vS : Valued S ℤₘ₀] [ValAlgebra R S] - -noncomputable def Index_of_G_i (u : ℚ) : ℚ := - if u ≥ (-1) then - relindex' G(S/R)_[0] G(S/R)_[(Int.ceil u)] - else - 1 - -noncomputable def varphi' (u : ℚ) : ℚ := - 1 / (Index_of_G_i R S u) - -noncomputable def varphi (u : ℚ) : ℚ := - if u ≥ 1 then - ∑ x in Finset.Icc 1 (Int.floor u), (varphi' R S x) + (u - (Int.floor u)) * (varphi' R S u) - else - u * (varphi' R S u) - -theorem varphi'_pos : ∀ u : ℚ , 0 < varphi' R S u := by - unfold varphi' Index_of_G_i relindex' index - rintro u - by_cases h : u ≥ -1 - simp [h] - apply div_pos_iff.2 - left - constructor <;> sorry - simp [h] - -theorem varphi_mono_int : ∀a1 a2 : ℤ , a1 < a2 → (varphi R S a1) < (varphi R S a2) := by - rintro a1 a2 h - induction' a2 with n ih - sorry - sorry - ---I will change this name -theorem varphi_lt_int_ceil : ∀a : ℚ , a ≠ (Int.ceil a) → (varphi R S a) < (varphi R S (Int.ceil a)) := by sorry - -theorem varphi_mono_section : ∀a1 a2 : ℚ , (Int.floor a1) = (Int.floor a2) ∧ (a1 > a2) → (varphi R S a1) > (varphi R S a2) := by - rintro a1 a2 ⟨h1, h2⟩ - apply gt_iff_lt.2 - apply sub_lt_zero.1 - have hsub: (varphi R S a2) - (varphi R S a1) = (a2 - a1) * (varphi' R S a1) := by - have h' : varphi' R S a1 = varphi' R S a2 := by - unfold varphi' Index_of_G_i - have hceil : Int.ceil a1 = Int.ceil a2 := by - sorry - sorry - unfold varphi - by_cases ha2 : 1 ≤ a2 - have : 1 ≤ a1 := by linarith [h2] - simp [ha2, this, h1, h'] - sorry - sorry - have hge: (varphi R S a2) - (varphi R S a1) < 0 := by - simp [hsub] - apply mul_neg_iff.2 - right - constructor - linarith [h2] - apply varphi'_pos R S - exact hge - -theorem varphi_mono : ∀a1 a2 : ℚ , a1 > a2 → (varphi R S a1) > (varphi R S a2) := by - rintro a1 a2 h - by_cases h1 : (Int.floor a1) = (Int.floor a2) - exact varphi_mono_section R S a1 a2 ⟨h1, h⟩ - have ha1 : varphi R S a1 ≥ varphi R S (Int.floor a1) := by - by_cases hequl : a1 = Int.floor a1 - nth_rw 1 [hequl] - have hgt : varphi R S a1 > varphi R S (Int.floor a1) := by - have hgt' : a1 > Int.floor a1 := by - sorry - apply varphi_mono_section R S a1 (Int.floor a1) ⟨rfl,hgt'⟩ - sorry - have h'' : Int.floor a1 > a2 := by - by_contra hngt - push_neg at hngt - have hflooreq : Int.floor a1 = Int.floor a2 := by - have hfloorle : Int.floor a1 ≤ Int.floor a2 := by - apply Int.le_floor.2 hngt - have hfloorge : Int.floor a2 ≤ Int.floor a1 := by - apply Int.floor_le_floor - apply le_of_lt - simp [h] - apply (LE.le.ge_iff_eq hfloorle).1 hfloorge - contradiction - have ha2 : varphi R S (Int.floor a1) > varphi R S a2 := by sorry - -- have hcllefl : Int.ceil a2 ≤ Int.floor a1 := by - -- apply Int.ceil_le.2 - -- apply le_of_lt h'' - -- by_cases heqceil : a2 = Int.ceil a2 - -- have hclltfl : Int.ceil a2 < Int.floor a1 := by - -- by_contra hn - -- push_neg at hn - -- have hcleqfl : Int.ceil a2 = Int.floor a1 := by - -- apply (LE.le.ge_iff_eq hcllefl).1 hn - -- have hfleqfl : Int.floor a1 = Int.floor a2 := by - -- sorry - -- contradiction - -- sorry --- have hphiclltfl : varphi R S (Int.ceil a2) < varphi R S (Int.floor a1) := by --- apply varphi_mono_int --- sorry --- -- assumption --- -- rw [heqceil] --- simp [hphiclltfl] --- have hflcl : varphi R S (Int.ceil a2) ≤ varphi R S (Int.floor a1) := by --- by_cases hfleqcl : Int.ceil a2 = Int.floor a1 --- simp [hfleqcl] --- have hflgtcl : Int.ceil a2 < Int.floor a1 := by --- push_neg at hfleqcl --- apply lt_of_le_of_ne hcllefl hfleqcl --- apply le_of_lt --- apply varphi_mono_int --- exact hflgtcl --- have hcl : varphi R S a2 < varphi R S (Int.ceil a2) := by --- push_neg at heqceil --- apply varphi_lt_int_ceil --- assumption - apply gt_of_ge_of_gt - apply ha1 - apply ha2 - -theorem varphi_bij : Function.Bijective (varphi R S) := by - constructor - rintro a1 a2 h - contrapose! h - by_cases h1 : a1 > a2 - have hlt : (varphi R S a2) < (varphi R S a1) := by - apply varphi_mono - apply h1 - apply ne_of_gt hlt - have hlt : (varphi R S a2) > (varphi R S a1) := by - apply varphi_mono - apply lt_of_not_ge - push_neg at * - exact lt_of_le_of_ne h1 h - apply ne_of_lt hlt - rintro b - unfold varphi varphi' - by_cases hb : b < 0 - sorry - sorry - -noncomputable def psi : ℚ → ℚ := - invFun (varphi R S) - -theorem psi_bij : Function.Bijective (psi R S) := by - constructor - have hpsi: (invFun (varphi R S)).Injective := - (rightInverse_invFun (varphi_bij R S).2).injective - exact hpsi - apply invFun_surjective - apply (varphi_bij R S).1 - -theorem varphi_zero_eq_zero : varphi R S 0 = 0 := by - unfold varphi - simp - ---do I really need this? -theorem varphi_negone_eq_negone : varphi R S (-1) = -1 := by - unfold varphi varphi' - simp - sorry - -noncomputable def psi' (v : ℚ): ℚ := - 1 / (varphi' R S (psi R S v)) - -theorem psi_zero_eq_zero : psi R S 0 = 0 := by - unfold psi - nth_rw 1 [← varphi_zero_eq_zero R S] - have : id 0 = (0 : ℚ) := by rfl - nth_rw 2 [← this] - have Inj : (varphi R S).Injective := by apply (varphi_bij R S).1 - rw [← invFun_comp Inj] - simp - ---lemma 3 -variable [Field R] [Field S] [Module R S] [FiniteDimensional R S] - -open scoped Classical - -theorem Varphi_eq_Sum_Inf (u : ℚ) [Fintype (S ≃ₐv[R] S)] : (varphi R S u) = (1 / Nat.card G(S/R)_[0]) * (∑ x : (S ≃ₐv[R] S) , ((ValAlgEquiv.truncatedLowerIndex R S x (u + 1))))- 1 := by - unfold varphi varphi' ValAlgEquiv.truncatedLowerIndex - by_cases h : u ≥ 1 - simp [h] - sorry - sorry diff --git a/RamificationGroup/Unused/Trash/test1.lean b/RamificationGroup/Unused/Trash/test1.lean deleted file mode 100644 index 826be60..0000000 --- a/RamificationGroup/Unused/Trash/test1.lean +++ /dev/null @@ -1,60 +0,0 @@ -import RamificationGroup.LowerNumbering -import Mathlib.RingTheory.Valuation.Basic -import RamificationGroup.Valuation.Trash.test - -open QuotientGroup IntermediateField DiscreteValuation Valued Valuation Subgroup Set - -variable (K L : Type*) {ΓK : outParam Type*} [Field K] [Field L] [LinearOrderedCommGroupWithZero ΓK] [vK : Valued K ΓK] [vS : Valued L ℤₘ₀] [ValAlgebra K L] {H : Subgroup (L ≃ₐ[K] L)} [Subgroup.Normal H] - -def Lift_Galois_ValEquiv : (L ≃ₐ[K] L) →* (L ≃ₐv[K] L) := by sorry - -def Galois_to_Quotient : (L ≃ₐ[(fixedField H)] L) →* (L ≃ₐ[K] L) ⧸ H := by sorry - -instance : Valued (fixedField H) ℤₘ₀ where - uniformContinuous_sub := sorry - v := sorry - is_topological_valuation := sorry - -attribute [-instance] Subtype.preorder -instance : ValAlgebra K (fixedField H) := -{ - algebra (fixedField H) with - monotone' := sorry - continuous_toFun := sorry - val_isEquiv_comap := sorry -} - -instance : ValAlgebra (fixedField H) L := -{ - Subalgebra.toAlgebra (fixedField H).toSubalgebra with - monotone' := sorry - continuous_toFun := sorry - val_isEquiv_comap := sorry -} - ---lemma 4 -theorem Varphi_With_i' (σ : (L ≃ₐ[(fixedField H)] L)) : (varphi K L (sSup (i_[L/K] '' ((Lift_Galois_ValEquiv K L) '' ((mk' H)⁻¹' {(Galois_to_Quotient K L σ)}))))) = (i_[L/(fixedField H)] ((Lift_Galois_ValEquiv (fixedField H) L) σ)) - (1 : ℕ∞) := by sorry - ---lemma 5 -theorem Herbrand_Thm {u : ℚ} {v : ℚ} (h : v = varphi K L u) : G(L/(fixedField H))_[(Int.ceil v)] = (_ ⧸ H.subgroupOf ((G(L/K)_[(Int.ceil u)].comap (Lift_Galois_ValEquiv K L)) ⊔ H)) := by sorry - -open Set -variable {u : ℚ} {σ : (L ≃ₐ[(fixedField H)] L)} {t : ((mk' H)⁻¹' {(Galois_to_Quotient K L σ)})} -#check (G(L/K)_[(Int.ceil u)].comap (Lift_Galois_ValEquiv K L)) -#check H -#check (G(L/K)_[(Int.ceil u)].comap (Lift_Galois_ValEquiv K L)) ⊔ H -#check H.subgroupOf ((G(L/K)_[(Int.ceil u)].comap (Lift_Galois_ValEquiv K L)) ⊔ H) -#check ((Lift_Galois_ValEquiv K L) t) -#check i_[L/K] ((Lift_Galois_ValEquiv K L) t) -#check (fun (t : ((mk' H)⁻¹' {(Galois_to_Quotient K L σ)})) => i_[L/K] ((Lift_Galois_ValEquiv K L) t)) -#check (i_[L/K] '' ((Lift_Galois_ValEquiv K L) '' ((mk' H)⁻¹' {(Galois_to_Quotient K L σ)}))) -#check sSup (i_[L/K] '' ((Lift_Galois_ValEquiv K L) '' ((mk' H)⁻¹' {(Galois_to_Quotient K L σ)}))) - ---prop 15 -theorem varphi_comp_field_ext : (varphi K (fixedField H)) ∘ (varphi (fixedField H) L) = varphi K L:= by sorry - -theorem psi_comp_field_ext : (psi K (fixedField H)) ∘ (psi (fixedField H) L) = psi K L:= by sorry - - -variable {H1 H2: Subgroup ((L ≃ₐ[K] L))} -#check H1 ⊔ H2 diff --git a/RamificationGroup/Unused/Trash/test2.lean b/RamificationGroup/Unused/Trash/test2.lean deleted file mode 100644 index 92b2479..0000000 --- a/RamificationGroup/Unused/Trash/test2.lean +++ /dev/null @@ -1,642 +0,0 @@ -import RamificationGroup.LowerNumbering -import Mathlib.MeasureTheory.Integral.IntervalIntegral -import Mathlib.GroupTheory.Index -import Mathlib.Logic.Function.Basic -import Mathlib.MeasureTheory.Measure.MeasureSpaceDef -import Mathlib.Algebra.BigOperators.Basic - ---definition of phi and psi - -open DiscreteValuation Subgroup Set Function MeasureTheory Finset BigOperators Int Valued - -variable (R S : Type*) {ΓR : outParam Type*} [CommRing R] [Ring S] [LinearOrderedCommGroupWithZero ΓR] [vR : Valued R ΓR] [vS : Valued S ℤₘ₀] [ValAlgebra R S] - -section - -variable {G : Type*} [Group G] (H L K : Subgroup G) - -noncomputable def relindex' : ℚ := - (K.index : ℚ) / (H.index: ℚ) - -end - - -noncomputable def Index_of_G_i (u : ℚ) : ℚ := - if u > (-1) then - relindex' G(S/R)_[0] G(S/R)_[(Int.ceil u)] - else - 1 - -noncomputable def phi' (u : ℚ) : ℚ := - 1 / (Index_of_G_i R S u) - -noncomputable def phi (u : ℚ) : ℚ := - if u ≥ 1 then - ∑ x in Finset.Icc 1 (Int.floor u), (phi' R S x) + (u - (Int.floor u)) * (phi' R S u) - else - u * (phi' R S u) - ---for mathlib -theorem sub_of_sum (a : ℤ) (f : ℚ → ℚ) (h : 1 ≤ a): ∑ x in Icc 1 (a + 1), f x - ∑ x in Icc 1 a, f x = f (a + 1) := by - have hncons : (a + 1) ∉ Finset.Icc 1 a := by simp - have hcons : (Finset.Icc 1 (a + 1)) = cons (a + 1) (Finset.Icc 1 a) hncons := by - ext n - simpa using (by omega) - rw [hcons] - rw [sum_cons] - simp - ---for mathlib -theorem ceil_eq_floor_add_one_iff (u : ℚ) (h : u ≠ ⌊u⌋) : ⌈u⌉ = ⌊u⌋ + 1 := by - have hu : fract u ≠ 0 := by - unfold fract - by_contra h' - have : u = ⌊u⌋ := by linarith [h'] - contradiction - have h' : ⌈u⌉ = u + 1 - Int.fract u := by - apply ceil_eq_add_one_sub_fract hu - unfold fract at h' - have h'': (⌈u⌉ : ℚ) = ((⌊u⌋ + 1) : ℚ):= by - rw [h'] - ring - exact_mod_cast h'' - ---for mathlib -theorem Int.eq_of_ge_of_lt_add_one (a m : ℤ) (h1 : m ≤ a) (h2 : a < (m + 1)) : a = m := by - have hle : a ≤ m + 1 - 1 := by apply le_sub_one_iff.2 h2 - simp at hle - apply ((LE.le.ge_iff_eq h1).1 hle).symm - -theorem phi'_eq_ceil : ∀ u : ℚ , phi' R S u = phi' R S ⌈u⌉ := by - rintro u - unfold phi' Index_of_G_i - by_cases h : -1 < u - · have hcl : ⌈u⌉ > (-1 : ℚ) := by - apply lt_of_lt_of_le - apply h - apply le_ceil - simp [h, hcl] - have hcl : ¬⌈u⌉ > (-1 : ℚ) := by - by_contra hc - have hcl' : -1 < ⌈u⌉ := by apply cast_lt.1 hc - have : -1 < u := by - apply lt_ceil.1 hcl' - contradiction - simp [h, hcl] - -theorem phi'_pos : ∀ u : ℚ , 0 < phi' R S u := by - unfold phi' Index_of_G_i relindex' index - rintro u - by_cases h : u > -1 - simp [h] - apply div_pos_iff.2 - left - constructor <;> sorry - simp [h] - -theorem phi'_neg_int_eq_one : ∀ u : ℤ , (u ≤ 0) → phi' R S u = 1 := by - rintro u hu - unfold phi' Index_of_G_i - by_cases hgt : (-1 : ℚ) < u - · simp [hgt] - have hzero : 0 = u := by - have hgt' : -1 < u := by apply cast_lt.1 hgt - have hge : -1 ≤ u - 1 := by - apply le_sub_one_iff.2 hgt' - simp at hge - apply (LE.le.ge_iff_eq hge).1 hu - have hzero' : u = (0 : ℚ) := by simp [hzero] - sorry - simp [hgt] - -theorem phi_int_succ : ∀a : ℤ , (phi R S a) = (phi R S (a + 1)) - (phi' R S (a + 1)) := by - rintro a - unfold phi - by_cases hgeone : (1 : ℚ) ≤ a - · have hgezero : (0 : ℚ) ≤ a := by linarith - simp [hgeone, hgezero] - have h : ∑ x in Icc 1 (a + 1), phi' R S ↑x = phi' R S (a + 1) + ∑ x in Icc 1 a, phi' R S ↑x := by - have hgeone' : 1 ≤ a := by apply cast_le.1 hgeone - have h' : ∑ x in Finset.Icc 1 (a + 1), phi' R S ↑x - ∑ x in Finset.Icc 1 a, phi' R S ↑x = phi' R S (↑a + 1) := by - apply sub_of_sum a (phi' R S) hgeone' - linarith [h'] - simp [h] - by_cases hgezero : (0 : ℚ) ≤ a - · have heqzero : (0 : ℚ) = a := by - --this - push_neg at hgeone - have hgeone' : a < 1 := by - apply cast_lt.1 hgeone - have hlezero : a ≤ (0 : ℚ) := by - convert le_sub_one_iff.2 hgeone' - simp - apply (LE.le.ge_iff_eq hgezero).1 hlezero - erw [←heqzero] - simp [hgeone, hgezero] - simp [hgeone, hgezero] - push_neg at * - ring - apply mul_eq_mul_left_iff.2 - left - rw [phi'_neg_int_eq_one] - have : (1 + a) ≤ 0 := by - have hgezero' : a < 0 := by apply cast_lt.1 hgezero - have hle: a ≤ 0 - 1 := by - convert le_sub_one_iff.2 hgezero' - linarith [hle] - symm - convert phi'_neg_int_eq_one R S (1 + a) this - simp - apply le_of_lt - apply cast_lt.1 hgezero - -theorem phi_mono_int : ∀a1 a2 : ℤ , a1 < a2 → (phi R S a1) < (phi R S a2) := by - rintro a1 a2 h - have hsub : a2 = a1 + (a2 - a1 - 1) + 1 := by ring - rw [hsub] - induction' a2 - a1 - 1 with n ih - · induction' n with n ih - · apply sub_lt_zero.1 - rw [phi_int_succ R S a1] - simp - apply phi'_pos - apply lt_trans - apply ih - simp - apply sub_lt_zero.1 - have heq : phi R S (↑a1 + ↑n + 1) = phi R S (↑a1 + (↑n + 1) + 1) - (phi' R S (a1 + n + 1 + 1)) := by - convert phi_int_succ R S (a1 + n + 1) - <;>simp - ring - rw [heq] - simp - apply phi'_pos - sorry - -theorem phi_mono_int' : ∀a1 a2 : ℤ , a1 ≤ a2 → (phi R S a1) ≤ (phi R S a2) := by - rintro a1 a2 h - by_cases heq : a1 = a2 - simp [heq] - apply le_of_lt - push_neg at * - have hlt : a1 < a2 := by apply lt_of_le_of_ne h heq - apply phi_mono_int R S a1 a2 hlt - ---i'll change this name -theorem phi_rational_floor : ∀ a : ℚ , (phi R S a) = (phi R S ⌊a⌋) + ((phi R S (⌊a⌋ + 1)) - (phi R S ⌊a⌋)) * (a - ⌊a⌋) := by - rintro a - unfold phi - by_cases ha : a ≥ 1 - · have hfl : (1 : ℚ) ≤ ⌊a⌋ := by - convert le_floor.2 ha - simp - apply cast_le - have hfl' : (0 : ℚ) ≤ ⌊a⌋ := by - linarith [hfl] - simp [ha, hfl, hfl'] - nth_rw 2 [mul_comm] - apply mul_eq_mul_left_iff.2 - by_cases hzero : fract a = 0 - · right - exact hzero - left - have h : ∑ x in Finset.Icc 1 (⌊a⌋ + 1), phi' R S ↑x - ∑ x in Finset.Icc 1 ⌊a⌋, phi' R S ↑x = phi' R S (⌊a⌋ + 1) := by - have hfl' : (1 : ℤ) ≤ ⌊a⌋ := by apply cast_le.1 hfl - apply sub_of_sum ⌊a⌋ (phi' R S) hfl' - rw [h, phi'_eq_ceil] - have hflcl : ⌈a⌉ = ⌊a⌋ + 1 := by - unfold fract at hzero - push_neg at hzero - have : a ≠ ⌊a⌋ := by - by_contra hc - have hc' : a - ⌊a⌋ = 0 := by linarith - contradiction - apply ceil_eq_floor_add_one_iff a this - rw [hflcl] - congr - simp - have hfl : ¬ (1 : ℚ) ≤ ↑⌊a⌋ := by - by_contra h' - have h'' : (1 : ℚ) ≤ a := by - apply le_floor.1 - convert h' - simp - apply cast_le.symm - contradiction - by_cases hzero : (0 : ℚ) ≤ ⌊a⌋ - · simp [ha, hfl, hzero] - push_neg at * - --and this is the same - have hflzero : 0 = ⌊a⌋ := by - have hfl' : ⌊a⌋ < 1 := by apply cast_lt.1 hfl - have hlezero : ⌊a⌋ ≤ 1 - 1 := by - apply le_sub_one_iff.2 hfl' - simp at hlezero - have hgezero : 0 ≤ ⌊a⌋ := by apply cast_le.1 hzero - apply (LE.le.ge_iff_eq hgezero).1 hlezero - unfold fract - simp [hflzero.symm] - rw [mul_comm] - apply mul_eq_mul_right_iff.2 - by_cases hzero' : a = 0 - · right - exact hzero' - left - have hcl : ⌈a⌉ = 1 := by - have hgtzero : (0 : ℚ) < a := by - apply lt_of_le_of_ne - have : ⌊a⌋ ≤ a := by apply floor_le - apply le_trans - apply hzero - apply this - push_neg at hzero' - apply hzero'.symm - apply ceil_eq_on_Ioc - simp - constructor - apply hgtzero - apply le_of_lt ha - rw [phi'_eq_ceil, hcl] - congr - simp [ha, hfl, hzero] - push_neg at * - sorry - - -theorem phi_rational_ceil : ∀ a : ℚ , (phi R S a) = (phi R S (⌊a⌋ + 1)) - ((phi R S (⌊a⌋ + 1)) - (phi R S ⌊a⌋)) * (⌊a⌋ - a + 1) := by - rintro a - unfold phi - by_cases ha : (1 : ℚ) ≤ a - · have hfl : (1 : ℚ) ≤ ⌊a⌋ := by - convert le_floor.2 ha - apply cast_le - have hcl : (1 : ℚ) ≤ (⌊a⌋ + 1) := by - linarith [hfl] - simp [ha, hcl, hfl] - have h : ∑ x in Finset.Icc 1 (⌊a⌋ + 1), phi' R S ↑x - ∑ x in Finset.Icc 1 ⌊a⌋, phi' R S ↑x = phi' R S (⌊a⌋ + 1) := by - have hfl' : (1 : ℤ) ≤ ⌊a⌋ := by apply cast_le.1 hfl - apply sub_of_sum ⌊a⌋ (phi' R S) hfl' - have h' : (∑ x in Finset.Icc 1 (⌊a⌋ + 1), phi' R S ↑x - ∑ x in Finset.Icc 1 ⌊a⌋, phi' R S ↑x) - fract a * phi' R S a - - (∑ x in Finset.Icc 1 (⌊a⌋ + 1), phi' R S ↑x - ∑ x in Finset.Icc 1 ⌊a⌋, phi' R S ↑x) * (↑⌊a⌋ - a + 1) = 0 := by - rw [h] - by_cases hfl' : a - ⌊a⌋ = 0 - · unfold fract - have : ⌊a⌋ - a = 0 := by linarith [hcl] - simp [hcl, this] - left - unfold fract - linarith [this] - push_neg at * - have hcl' : (⌈a⌉ : ℚ) = (⌊a⌋ : ℚ) + 1:= by - have hfl'' : a ≠ ⌊a⌋ := by - by_contra hc - have : a - ⌊a⌋ = 0 := by linarith [hc] - contradiction - have hcl'' : ⌈a⌉ = ⌊a⌋ + 1:= by - apply ceil_eq_floor_add_one_iff a hfl'' - sorry - ring - nth_rw 3 [phi'_eq_ceil] - unfold fract - have heq : phi' R S (1 + ⌊a⌋) = phi' R S ⌈a⌉ := by - rw [hcl'] - have : 1 + (⌊a⌋ : ℚ) = (⌊a⌋ : ℚ) + 1 := by ring - rw [this] - rw [heq] - ring - linarith [h'] - have hfl : ¬(1 : ℚ) ≤ ⌊a⌋ := by - by_contra hc - have hge : (1 : ℚ) ≤ a := by - apply le_floor.1 - convert hc - simp - apply cast_le.symm - contradiction - by_cases hcl : (1 : ℚ) ≤ (⌊a⌋ + 1) - · simp [ha, hcl, hfl] - push_neg at * - have hfl' : ⌊a⌋ = 0 := by - simp at hcl - have hfl' : ⌊a⌋ < 1 := by apply cast_lt.1 hfl - apply Int.eq_of_ge_of_lt_add_one ⌊a⌋ 0 hcl hfl' - simp [hfl'] - by_cases hzero : a = 0 - · simp [hzero] - have h : phi' R S a = phi' R S 1 := by - have h' : phi' R S a = phi' R S ⌈a⌉ := by - apply phi'_eq_ceil - rw [h'] - have hcl' : ⌈a⌉ = (1 : ℚ) := by - have hnefl : a ≠ ⌊a⌋ := by - rw [hfl'] - push_neg at hzero - apply hzero - have : ⌈a⌉ = ⌊a⌋ + 1 := by - apply ceil_eq_floor_add_one_iff a hnefl - rw [this] - simp [hfl'] - rw [hcl'] - ring - simp [h] - simp [ha, hcl, hfl] - push_neg at * - sorry - -theorem phi_gt_floor : ∀ a : ℚ , (a ≠ ⌊a⌋) → (phi R S a) > (phi R S ⌊a⌋) := by - rintro a ha - apply gt_iff_lt.2 - apply sub_lt_zero.1 - nth_rw 2 [phi_rational_floor] - simp - apply mul_pos_iff.2 - left - constructor - simp - convert phi_mono_int R S ⌊a⌋ (⌊a⌋ + 1) (by simp) - simp - apply fract_pos.2 ha - -theorem phi_lt_ceil : ∀ a : ℚ , (phi R S a) < (phi R S (⌊a⌋ + 1)) := by - rintro a - apply gt_iff_lt.2 - apply sub_lt_zero.1 - nth_rw 1 [phi_rational_ceil] - simp - apply mul_pos_iff.2 - left - constructor - simp - convert phi_mono_int R S ⌊a⌋ (⌊a⌋ + 1) (by simp) - simp - have h : a - 1 < ⌊a⌋ := by apply sub_one_lt_floor - linarith [h] - -theorem phi_mono_in_section : ∀ a1 a2 : ℚ , (⌊a1⌋ = ⌊a2⌋) ∧ (a1 < a2) → (phi R S a1) < (phi R S a2) := by - rintro a1 a2 ⟨h1, h2⟩ - apply gt_iff_lt.2 - apply sub_lt_zero.1 - nth_rw 2 [phi_rational_floor] - nth_rw 1 [phi_rational_floor] - rw [h1] - simp - apply sub_lt_zero.1 - have : ((phi R S (↑⌊a2⌋ + 1)) - (phi R S ↑⌊a2⌋)) * (a1 - ↑⌊a2⌋) - ((phi R S (↑⌊a2⌋ + 1)) - (phi R S ↑⌊a2⌋)) * fract a2 = ((phi R S (↑⌊a2⌋ + 1)) - (phi R S ↑⌊a2⌋)) * (a1 - a2) := by - unfold fract - calc - ((phi R S (↑⌊a2⌋ + 1)) - (phi R S ↑⌊a2⌋)) * (a1 - ↑⌊a2⌋) - ((phi R S (↑⌊a2⌋ + 1)) - (phi R S ↑⌊a2⌋)) * (a2 - ⌊a2⌋) = ((phi R S (↑⌊a2⌋ + 1)) - (phi R S ↑⌊a2⌋)) * ((a1 - ⌊a2⌋) - (a2 - ⌊a2⌋)) := by - ring - _ = ((phi R S (↑⌊a2⌋ + 1)) - (phi R S ↑⌊a2⌋)) * (a1 - a2) := by - simp - left - unfold fract - ring - rw [this] - apply mul_neg_iff.2 - left - constructor - simp - convert phi_mono_int R S ⌊a2⌋ (⌊a2⌋ + 1) (by simp) - simp - simp [h2] - ---i'll change this name too -theorem phi_mono_over_section : ∀ a1 a2 : ℚ , (⌊a1⌋ ≠ ⌊a2⌋) ∧ (a1 < a2) → (phi R S a1) < (phi R S a2) := by - rintro a1 a2 ⟨hne, hlt⟩ - by_cases hfloor : a2 = ⌊a2⌋ - have hle : ⌊a1⌋ + 1 ≤ ⌊a2⌋ := by - have hlt : ⌊a1⌋ < ⌊a2⌋ := by - apply lt_of_le_of_ne - apply floor_le_floor - apply le_of_lt hlt - apply hne - apply add_one_le_of_lt hlt - apply lt_of_lt_of_le - have h1 : (phi R S a1) < (phi R S (⌊a1⌋ + 1)) := by apply (phi_lt_ceil R S) - apply h1 - have h2 : (phi R S (⌊a1⌋ + 1)) ≤ (phi R S a2) := by - by_cases heq : (⌊a1⌋ + 1) = a2 - simp [heq] - push_neg at heq - have h1' : (phi R S (⌊a1⌋ + 1)) ≤ (phi R S ⌊a2⌋) := by - convert phi_mono_int' R S (⌊a1⌋ + 1) ⌊a2⌋ hle - simp - rw [hfloor] - exact h1' - apply h2 - have hle : a1 ≤ ⌊a2⌋ := by - by_contra hc - push_neg at * - have h : ⌊a1⌋ = ⌊a2⌋ := by - have h1 : ⌊a1⌋ ≤ ⌊a2⌋ := by - apply floor_le_floor - apply le_of_lt - exact hlt - have h2 : ⌊a2⌋ ≤ ⌊a1⌋ := by - apply le_floor.2 - apply le_of_lt hc - apply (LE.le.ge_iff_eq h1).1 h2 - contradiction - have hlt : ⌊a2⌋ < a2 := by - have hge : ⌊a2⌋ ≤ a2 := by apply floor_le - push_neg at hfloor - apply lt_of_le_of_ne hge hfloor.symm - apply lt_of_le_of_lt - have h1 : (phi R S a1) ≤ (phi R S ⌊a2⌋) := by - by_cases heq : a1 = ⌊a2⌋ - simp [heq] - apply le_of_lt - apply lt_of_lt_of_le - push_neg at * - have hlt' : a1 < ⌊a2⌋ := by apply lt_of_le_of_ne hle heq - have h1' : (phi R S a1) < (phi R S (⌊a1⌋ + 1)) := by apply phi_lt_ceil R S - apply h1' - have hle' : ⌊a1⌋ + 1 ≤ ⌊a2⌋ := by - push_neg at * - have hlt' : ⌊a1⌋ < ⌊a2⌋ := by - have hle'' : ⌊a1⌋ ≤ ⌊a2⌋ := by - apply floor_le_floor - apply le_of_lt - assumption - apply lt_of_le_of_ne hle'' hne - apply Int.le_of_lt_add_one - linarith [hlt'] - have h2' : (phi R S ↑(⌊a1⌋ + 1)) ≤ (phi R S (⌊a2⌋)) := by - apply phi_mono_int' R S (⌊a1⌋ + 1) ⌊a2⌋ hle' - convert h2' - simp - apply h1 - push_neg at hfloor - have h2 : (phi R S ⌊a2⌋) < (phi R S a2) := by apply (phi_gt_floor R S a2 hfloor) - apply h2 - -theorem phi_mono_iff : (∀a1 a2 : ℚ , a1 < a2 → (phi R S a1) < (phi R S a2)) ↔ (∀a1 a2 : ℤ , a1 < a2 → (phi R S a1) < (phi R S a2)) := by - constructor - rintro h a1 a2 - apply phi_mono_int R S a1 a2 - rintro h a1 a2 h' - by_cases hfloor : ⌊a1⌋ = ⌊a2⌋ - apply phi_mono_in_section - constructor <;> assumption - push_neg at * - apply phi_mono_over_section - constructor <;> assumption - -theorem phi_mono : ∀a1 a2 : ℚ , a1 < a2 → (phi R S a1) < (phi R S a2) := by - apply (phi_mono_iff R S).2 - apply phi_mono_int - -theorem phi_bij : Function.Bijective (phi R S) := by - constructor - rintro a1 a2 h - contrapose! h - by_cases h1 : a1 > a2 - have hlt : (phi R S a2) < (phi R S a1) := by - apply phi_mono - apply h1 - apply ne_of_gt hlt - have hlt : (phi R S a2) > (phi R S a1) := by - apply phi_mono - apply lt_of_not_ge - push_neg at * - exact lt_of_le_of_ne h1 h - apply ne_of_lt hlt - rintro b - unfold phi phi' - by_cases hb : b < 0 - sorry - sorry - -noncomputable def psi : ℚ → ℚ := - invFun (phi R S) - -theorem psi_bij : Function.Bijective (psi R S) := by - constructor - have hpsi: (invFun (phi R S)).Injective := - (rightInverse_invFun (phi_bij R S).2).injective - exact hpsi - apply invFun_surjective - apply (phi_bij R S).1 - -theorem phi_zero_eq_zero : phi R S 0 = 0 := by - unfold phi - simp - -noncomputable def psi' (v : ℚ): ℚ := - 1 / (phi' R S (psi R S v)) - -theorem psi_zero_eq_zero : psi R S 0 = 0 := by - unfold psi - nth_rw 1 [← phi_zero_eq_zero R S] - have : id 0 = (0 : ℚ) := by rfl - nth_rw 2 [← this] - have Inj : (phi R S).Injective := by apply (phi_bij R S).1 - rw [← invFun_comp Inj] - simp - -theorem phi_inv_psi : ∀ a : ℚ , phi R S (psi R S a) = a := by - rintro a - apply invFun_eq - apply (phi_bij R S).surjective - ---lemma 3 -open scoped Classical - - -variable (K L : Type*) {ΓK : outParam Type*} [Field K] [Field L] [LinearOrderedCommGroupWithZero ΓK] [vK : Valued K ΓK] [vS : Valued L ℤₘ₀] [ValAlgebra K L] - -instance : Fintype (L ≃ₐv[K] L) where - elems := by sorry - complete := by sorry - -#check Finset.sum_disjiUnion -#check Set.PairwiseDisjoint -#check disjiUnion -#check Finset (Subgroup (L ≃ₐv[K] L)) -#check Finset (L ≃ₐv[K] L) -#check Finset G(L/K)_[10] -#check ((G(L/K)_[10] : Set (L ≃ₐv[K] L)) \ (G(L/K)_[11] : Set (L ≃ₐv[K] L))).toFinset -#check SDiff -#check (G(L/K)_[(-1)] : Set (L ≃ₐv[K] L)).toFinset - -noncomputable def G_diff (i : ℤ) : Finset (L ≃ₐv[K] L) := ((G(L/K)_[i] : Set (L ≃ₐv[K] L)) \ (G(L/K)_[(i + 1)] : Set (L ≃ₐv[K] L))).toFinset - -theorem G_pairwiseDisjoint (n : ℤ) : (PairwiseDisjoint (↑(Finset.Icc (-1) (n - 1))) (G_diff K L)) := by - induction' n with n ih - induction' n with n ih - simp - sorry - sorry - -theorem G_n_or_G_lt_n {n : ℤ} (x : (L ≃ₐv[K] L)) (h : x ∉ G(L/K)_[n]) : ∃ a, (-1 ≤ a ∧ a ≤ n - 1) ∧ x ∈ G_diff K L a := by - sorry - -theorem G_split (n : ℤ) : (⊤ : Finset (L ≃ₐv[K] L)) = (disjiUnion (Finset.Icc (-1) (n - 1)) (G_diff K L) (G_pairwiseDisjoint K L n)) ∪ (G(L/K)_[n] : Set (L ≃ₐv[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 x h - simp - -theorem Sum_Trunc_lower_Index_of_G_n (n : ℤ) (u : ℚ) (h : u ≤ n) : (Finset.sum (G(L/K)_[n] : Set (L ≃ₐv[K] L)).toFinset ((ValAlgEquiv.truncatedLowerIndex K L (u + 1) ·))) = (u + 1) * (Nat.card (G(L/K)_[n])) := by - calc - (Finset.sum (G(L/K)_[n] : Set (L ≃ₐv[K] L)).toFinset ((ValAlgEquiv.truncatedLowerIndex K L (u + 1) ·))) = Finset.sum (G(L/K)_[n] : Set (L ≃ₐv[K] L)).toFinset (fun (x : _) => u + 1) := by - apply sum_equiv (.refl (L ≃ₐv[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) ((ValAlgEquiv.truncatedLowerIndex K L (u + 1) ·))) = (n + 1) * (Nat.card (G_diff K L n)) := by - calc - (Finset.sum (G_diff K L n) ((ValAlgEquiv.truncatedLowerIndex K L (u + 1) ·))) = (Finset.sum (G_diff K L n) (fun (x : _) => ((n : ℚ) + 1))) := by - apply sum_equiv (.refl (L ≃ₐv[K] L)) - simp - rintro s hs - sorry - _ = (n + 1) * (Nat.card (G_diff K L n)) := by - norm_num - ring - -theorem Varphi_eq_Sum_Inf (u : ℚ) : (phi K L u) = (1 / Nat.card G(L/K)_[0]) * ((Finset.sum (⊤ : Finset (L ≃ₐv[K] L)) (ValAlgEquiv.truncatedLowerIndex K L (u + 1) ·))) - 1 := by - by_cases h : u ≥ 1 - · simp [h] - have hsplit : (Finset.sum (⊤ : Finset (L ≃ₐv[K] L)) (ValAlgEquiv.truncatedLowerIndex K L (u + 1) ·)) = (Finset.sum (((disjiUnion (Finset.Icc (-1) (⌈u⌉ - 1)) (G_diff K L) (G_pairwiseDisjoint K L _)))) ((ValAlgEquiv.truncatedLowerIndex K L (u + 1) ·))) + (Finset.sum (((G(L/K)_[(⌈u⌉)] : Set (L ≃ₐv[K] L)).toFinset)) ((ValAlgEquiv.truncatedLowerIndex K L (u + 1) ·))) := by - calc - (Finset.sum (⊤ : Finset (L ≃ₐv[K] L)) (ValAlgEquiv.truncatedLowerIndex K L (u + 1) ·)) = (Finset.sum (((disjiUnion (Finset.Icc (-1) (⌈u⌉ - 1)) (G_diff K L) (G_pairwiseDisjoint K L _)) ∪ (G(L/K)_[(⌈u⌉)] : Set (L ≃ₐv[K] L)).toFinset)) ((ValAlgEquiv.truncatedLowerIndex K L (u + 1) ·))) := by - congr - apply G_split - _ = (Finset.sum (((disjiUnion (Finset.Icc (-1) (⌈u⌉ - 1)) (G_diff K L) (G_pairwiseDisjoint K L _)))) ((ValAlgEquiv.truncatedLowerIndex K L (u + 1) ·))) + (Finset.sum (((G(L/K)_[(⌈u⌉)] : Set (L ≃ₐv[K] L)).toFinset)) ((ValAlgEquiv.truncatedLowerIndex K L (u + 1) ·))) := by - have : Disjoint (disjiUnion (Finset.Icc (-1) (⌈u⌉ - 1)) (G_diff K L) (G_pairwiseDisjoint K L _)) (toFinset ↑ G(L/K)_[⌈u⌉]) := by sorry - apply sum_union - apply this - have hsplit' : (Finset.sum (((disjiUnion (Finset.Icc (-1) (⌈u⌉ - 1)) (G_diff K L) (G_pairwiseDisjoint K L _)))) ((ValAlgEquiv.truncatedLowerIndex K L (u + 1) ·))) = Finset.sum _ fun (i : ℤ) => Finset.sum _ fun (x : _) => (ValAlgEquiv.truncatedLowerIndex K L (u + 1) x) := by - apply sum_disjiUnion - simp at hsplit hsplit' - rw [hsplit, hsplit'] - have hu : (Finset.sum ((G(L/K)_[(⌈u⌉)] : Set (L ≃ₐv[K] L)).toFinset) ((ValAlgEquiv.truncatedLowerIndex K L (u + 1) ·))) = (u + 1) * (Nat.card G(L/K)_[⌈u⌉]) := by - convert Sum_Trunc_lower_Index_of_G_n K L ⌈u⌉ u (by apply le_ceil) - rw [hu] - have hd : Finset.sum (Finset.Icc (-1) (⌈u⌉ - 1)) (fun (i : ℤ) => Finset.sum (G_diff K L i) (fun (x : _) => (ValAlgEquiv.truncatedLowerIndex K L (u + 1) x))) = Finset.sum (Finset.Icc (-1) (⌈u⌉ - 1)) fun (i : ℤ) => (i + 1) * (Nat.card ((G(L/K)_[i] : Set (L ≃ₐv[K] L)) \ G(L/K)_[(i + 1)] : Set (L ≃ₐv[K] L))):= by - norm_num - apply sum_equiv (.refl ℤ) - simp - simp - rintro i hge hle - have hle' : i ≤ u := by - sorry - convert Sum_Trunc_lower_Index_of_diff_G K L i u hle' - unfold G_diff - simp - sorry - rw [hd] - sorry - unfold phi - simp [h] - sorry diff --git a/RamificationGroup/Unused/Trash/truncated.lean b/RamificationGroup/Unused/Trash/truncated.lean deleted file mode 100644 index d1ceedc..0000000 --- a/RamificationGroup/Unused/Trash/truncated.lean +++ /dev/null @@ -1,21 +0,0 @@ -import RamificationGroup.LowerNumbering - -open DiscreteValuation Valued Valuation - -variable (R S : Type*) {ΓR : outParam Type*} [CommRing R] [Ring S] [LinearOrderedCommGroupWithZero ΓR] [vR : Valued R ΓR] [vS : Valued S ℤₘ₀] [ValAlgebra R S] - -theorem lowerindex_ge_iff_lowerramificationGroup (s : (S ≃ₐv[R] S)) {i : ℕ} : i_[S/R] s ≥ i + 1 ↔ s ∈ G(S/R)_[i] := by sorry - -theorem lowerindex_eq_iff_lowerramificationGroup (s : (S ≃ₐv[R] S)) {i : ℕ} : i_[S/R] s = i + 1 ↔ s ∈ G(S/R)_[i] ∧ s ∉ G(S/R)_[(i + 1)] := by sorry - -theorem lowerramificationGroup_has_top : ∃ n₀ : ℕ , ∀ n : ℕ , n ≥ n₀ → G(S/R)_[n] = {1 : (S ≃ₐv[R] S)} := by sorry - -noncomputable def ValAlgEquiv.TruncatedlowerIndex (s : (S ≃ₐv[R] S)) : ℕ := - sorry - -scoped [DiscreteValuation] notation:max " i_[" S:max "/" R:max "]ₜ" => ValAlgEquiv.TruncatedlowerIndexlowerIndex R S - -noncomputable def ValAlgEquiv.truncatedlowerIndex (s : (S ≃ₐv[R] S)) (u : ℕ): ℕ := - if h : i_[S/R] s = ⊤ then u - else if (i_[S/R] s) > u then u - else (i_[S/R] s).untop h diff --git a/RamificationGroup/Unused/ValuePreserved.lean b/RamificationGroup/Unused/ValuePreserved.lean deleted file mode 100644 index d9bf725..0000000 --- a/RamificationGroup/Unused/ValuePreserved.lean +++ /dev/null @@ -1,97 +0,0 @@ -/- -# of WARNINGs : 1 --/ - -import RamificationGroup.Valued.Defs -import LocalClassFieldTheory.DiscreteValuationRing.Extensions -import RamificationGroup.ForMathlib.Henselian - -variable {K : Type*} {ΓK : outParam Type*} [Field K] - [LinearOrderedCommGroupWithZero ΓK] [vK : Valued K ΓK] -variable {L : Type*} [Field L] - -namespace Valuation - -variable [Algebra K L] [FiniteDimensional K L] - -section int_closure - -variable {Γ : outParam Type*} [LinearOrderedCommGroupWithZero Γ] - {v : Valuation L Γ} - -theorem integral_closure_eq_integer_of_helselian [HenselianLocalRing vK.valuationSubring] - (h : vK.v.IsEquiv <| v.comap (algebraMap K L)) : - (integralClosure vK.v.valuationSubring L).toSubring = v.integer := by - sorry - -/-- WARNING : not mathematically true? more conditions? -/ -instance ___false___HenselianOfComplete [CompleteSpace K] : HenselianLocalRing vK.valuationSubring := by - sorry - -theorem integral_closure_eq_integer_of_complete_of_ext [CompleteSpace K] - (h : vK.v.IsEquiv <| v.comap (algebraMap K L)) : - (integralClosure vK.v.valuationSubring L).toSubring = v.integer := by - sorry - -end int_closure - -section value_ext - -variable [CompleteSpace K] -variable {Γ₁ Γ₂ : outParam Type*} [LinearOrderedCommGroupWithZero Γ₁] [LinearOrderedCommGroupWithZero Γ₂] - {v₁ : Valuation L Γ₁} {v₂ : Valuation L Γ₂} - -theorem unique_valuationSubring_of_ext (h₁ : vK.v.IsEquiv <| v₁.comap (algebraMap K L)) - (h₂ : vK.v.IsEquiv <| v₂.comap (algebraMap K L)) : - v₁.valuationSubring = v₂.valuationSubring := by - ext - rw [Valuation.mem_valuationSubring_iff, Valuation.mem_valuationSubring_iff, - ← Valuation.mem_integer_iff, ← Valuation.mem_integer_iff, - ← integral_closure_eq_integer_of_complete_of_ext h₁, ← integral_closure_eq_integer_of_complete_of_ext h₂] - -theorem unique_val_of_ext (h₁ : vK.v.IsEquiv <| v₁.comap (algebraMap K L)) - (h₂ : vK.v.IsEquiv <| v₂.comap (algebraMap K L)) : - v₁.IsEquiv v₂ := - (Valuation.isEquiv_iff_valuationSubring _ _).mpr <| unique_valuationSubring_of_ext h₁ h₂ - - -end value_ext - -end Valuation - -namespace ValAlgEquiv - -section alg_end -variable {ΓL : outParam Type*} [LinearOrderedCommGroupWithZero ΓL] [vL : Valued L ΓL] -variable [ValAlgebra K L] [FiniteDimensional K L] [CompleteSpace K] - -theorem algEnd_preserve_val (f : L →ₐ[K] L) : vL.v.IsEquiv <| vL.v.comap f := by - apply Valuation.unique_val_of_ext (K := K) - · apply ValAlgebra.val_isEquiv_comap - · rw [Valuation.isEquiv_iff_val_le_one] - simp; intro x - rw [← Valuation.comap_apply (algebraMap K L)] - revert x - rw [← Valuation.isEquiv_iff_val_le_one] - apply ValAlgebra.val_isEquiv_comap - - -theorem algEquiv_preserve_val (f : L ≃ₐ[K] L) : vL.v.IsEquiv <| vL.v.comap f := algEnd_preserve_val f.toAlgHom - -variable (K L) in -def fromAlgEquiv : (L ≃ₐ[K] L) →* (L ≃ₐv[K] L) where - toFun := fun f ↦ mk' f <| algEquiv_preserve_val f - map_one' := rfl - map_mul' := sorry - -variable (K L) in -def equivAlgEquiv : (L ≃ₐ[K] L) ≃* (L ≃ₐv[K] L) where - toFun := fromAlgEquiv K L - invFun := toAlgEquiv - left_inv := sorry - right_inv := sorry - map_mul' := sorry - -end alg_end - -end ValAlgEquiv diff --git a/RamificationGroup/Unused/Valued/Defs.lean b/RamificationGroup/Unused/Valued/Defs.lean deleted file mode 100644 index 91d4f87..0000000 --- a/RamificationGroup/Unused/Valued/Defs.lean +++ /dev/null @@ -1,112 +0,0 @@ -import LocalClassFieldTheory.DiscreteValuationRing.Basic - -open Valuation DiscreteValuation - -section check -variable {K} [Field K] {Γ : outParam Type*} [LinearOrderedCommGroupWithZero Γ] [vK : Valued K ℤₘ₀] - -#check [IsDiscrete vK.v] -- use this for discrete valuation - -#check Valuation.valuationSubring -- use this for `𝒪[K]` -#check Valuation.integer -- only subring, do not need K to be a field - -end check - -namespace Valued - -section Preorder - -variable {R : Type*} {Γ : outParam Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ] [Valued R Γ] - --- the preoder lift from valuation is different from the proorder of divisibility -- there is a preorder on the valuations, called specialization? -instance preorder : Preorder R := Valuation.toPreorder Valued.v - -theorem le_iff_val_le (x y : R) : x ≤ y ↔ v x ≤ v y := sorry - -theorem lt_iff_val_lt (x y : R) : x < y ↔ v x < v y := sorry - -theorem le_one_iff_val_le_one (x y : R) : x ≤ 1 ↔ v x ≤ 1 := sorry - -theorem lt_one_iff_val_lt_one (x y : R) : x < 1 ↔ v x < 1 := sorry - -theorem zero_le (x y : R) : 0 ≤ x := sorry - --- lower TODO : `theorems that x + y ≤ x, x + y < x,...` - -end Preorder - - -/-- An `Valued` version of `Valuation.valuationSubring`, it serves for the notation `𝒪[K]` -/ -@[reducible] -def valuationSubring (K : Type*) [Field K] {Γ : outParam Type*} [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] : ValuationSubring K := (Valued.v).valuationSubring - -scoped notation:max " 𝒪[" K:max "] " => Valued.valuationSubring K - - - -section IntegerValued -variable (R K : Type*) [Ring R] [Field K] {Γ : outParam Type*} [LinearOrderedCommGroupWithZero Γ] [vR : Valued R Γ] [vK : Valued K Γ] - ---`Is this really needed now? when there is no need for ValHom` --- is this instance OK? or is it needed? If needed add simp lemmas saying `v (s.liftInteger x) = v (s x.val) ` -instance integer.valued: Valued vR.v.integer Γ := Valued.mk' (vR.v.comap vR.v.integer.subtype) - - --- need to add this, lean cannot infer this --- `This will be auto infered once Valuation.valuationSubring is with @[reducible] tag`, for now, every instance need to be written again for `𝒪[K]`, in this file and Hom.lift file and more. This is also the reason that valuationSubring should with tag @[reducible]. Add this tag to `Valuation.valuationSubring` when impoet to mathlib! -instance valuationSubring.valued: Valued 𝒪[K] Γ := inferInstanceAs (Valued vK.v.integer Γ) - -#synth Valued 𝒪[K] Γ -#synth LocalRing 𝒪[K] -#synth Algebra 𝒪[K] K - - -/- -- For `Valued.liftInteger` -theorem integer_valuation_eq : (Valued.integer.valued R).v = (vR.v.comap vR.v.integer.subtype) := rfl - -theorem integerAlgebraMap.monotone : Monotone (algebraMap 𝒪[K] K) := sorry - --- also value IsEquiv of O[K] and K -- they are equal! --- `First show val is equiv, then use theorem IsEquiv implies monotone and continuous!!!!!` --/ - -@[simp] -theorem integer_val_coe (x : vR.v.integer) : Valued.v x = Valued.v (x : R) := rfl - -@[simp] -theorem valuationSubring_val_coe (x : 𝒪[K]): v x = v (x : K) := rfl - -theorem integer_val_le_one (x : vR.v.integer) : Valued.v x ≤ 1 := (mem_integer_iff vR.v x.1).mp x.2 - -#check mem_integer_iff - -end IntegerValued - - --- `theorems about the relation between order and valuation?` - -/-- An abbrevation for `LocalRing.maximalIdeal 𝒪[K]` of a `Valued` instance, it serves for notation `𝓂[K]` -/ -@[reducible] -def maximalIdeal (K : Type*) [Field K] {Γ : outParam Type*} [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] : Ideal 𝒪[K] := LocalRing.maximalIdeal 𝒪[K] - -scoped notation:max " 𝓂[" K:max "] " => maximalIdeal K - -/- -theorem maximalIdeal_eq {K : Type*} [Field K] {Γ : outParam Type*} [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] : 𝓂[K] = (Valued.v).ltIdeal 1 := sorry --/ - -/-- An abbrevation for `LocalRing.ResidueField 𝒪[K]` of a `Valued` instance, it serves for notation `𝓀[K]` -/ -@[reducible] -def ResidueField (K : Type*) [Field K] {Γ : outParam Type*} [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] := LocalRing.ResidueField (𝒪[K]) - -scoped notation:max " 𝓀[" K:max "] " => ResidueField K - -/- -- is this needed? -instance valuationSubring.coeResidueField {K : Type*} {Γ : outParam Type*} [LinearOrderedCommGroupWithZero Γ] [Field K] [Valued K Γ] : Coe 𝒪[K] 𝓀[K] where - coe := LocalRing.residue 𝒪[K] --/ - --- TODO? : Should residue field be equipped with trivial valuation? --- A generalization of this could be : after a valued ring quotient a "upper-closed" value ideal, it is equipped with a quotient valuation - -end Valued diff --git a/RamificationGroup/Unused/Valued/Hom/Defs.lean b/RamificationGroup/Unused/Valued/Hom/Defs.lean deleted file mode 100644 index 376c2d2..0000000 --- a/RamificationGroup/Unused/Valued/Hom/Defs.lean +++ /dev/null @@ -1,1032 +0,0 @@ -import RamificationGroup.Unused.Valued.Defs - -/-! -# ValRingHom and ValAlgebra - -In this file we define the type of ring homomorphisms that respect the valuation structure. We require such a homomorphism from valued ring `R` to valued ring `S` to satisfy the condition that the valuation on `R` is equivalent to the pullback of the valuation on `S`. This is strictly stronger than merely requiring `v x ≤ v y → v (f x) ≤ v (f y)`. - -## Main definitions - -* `ValRingHom` : Valued ring homomorphisms. -* `ValRingEquiv` : Valued ring isomorphisms. -* `ValAlgebra` -* `ValAlgHom` -* `ValAlgEquiv` - -## Notations - -* `→+*v`: Valued ring homomorphisms. -* `≃+*v`: Valued ring isomorphisms. -* `A →ₐv[R] B` -* `A ≃ₐv[R] B` - -## Implementation notes - - -## Tags - -valued ring homomorphism, valued homomorphism - --/ - --- `Consider K → K [[X]] , K is a local field, K[X] with valuation trivial on K, valuation ideal given by (X). This satisfies v x ≤ v y → v f x ≤ v f y` --- if the first definition K of local field K can have many valuation on L. second will pin down the valuation on L --- if as first choice, order preserving <=> valuation preserving <=> continuous (v(x) < 1 -> v f x < 1, by x^n -> 0 -> f x ^n -> 0) --- preorder on the set of valuations? not a type, IsSpecialization - --- TODO : Split these into 3 files(?) .ValAlgebra.Hom, .ValAlgebra.Basic --- TODO : SubValRing SubValAlgebra, SubValAlgebraClass, intermediate field shoul be SubValAlgebraClass instance. --- Question : whether the order should be included as part of the data of Valued instance? not an instance derived from Valued. --- TODO : Coe lemmas, how should they be arranged? --- Not TODO : scalartower do not need a val version. [IsScalarTower R S T] + [ValAlgebra R S] + [ValAlgebra S T] contains enough information --- TODO (?) : SubValRing gives ValAlgbra instance, what instance of valued should subalgebra be equipped? This always conflicts with DIscrete valuation in the local field case -open DiscreteValuation Valuation Valued - -section ValRingHom_ValRingEquiv - -section Hom - --- Valuation on B is an extension of valuation on A. -/-- `ValRingHom R S` is the type of ring homomorphisms that preserves valuation from valued ring `R` to valued ring `S`. - -Please note that the definition requires `v x ≤ v y ↔ v (f x) ≤ v (f y)` instead of `v x ≤ v y → v (f x) ≤ v (f y)`. For the latter case, one can use order-preserving ring homomorphisms. - -When possible, instead of parametrizing results over `(f : ValRingHom R S)`, -you should parametrize over `(F : Type*) [ValRingHomClass F R S] (f : F)`. - -When you extend this structure, make sure to extend `ValRingHomClass`. --/ -- mimicked from `OrderRingHom` -structure ValRingHom (R S : Type*) {ΓR ΓS : outParam Type*} [Ring R] [Ring S] - [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓS] - [vR : Valued R ΓR] [vS : Valued S ΓS] - extends OrderRingHom R S, ContinuousMap R S where - /-- The proposition that the ring map preserves valuation. -/ - val_isEquiv_comap' : vR.v.IsEquiv (vS.v.comap toRingHom) - -/-- Reinterpret a valued ring homomorphism into a ordered ring homomorphism. -/ -add_decl_doc ValRingHom.toOrderRingHom - -attribute [coe] ValRingHom.toOrderRingHom - -@[inherit_doc] -infixr:25 " →+*v " => ValRingHom -- 25 = Binding power of `→+*` - -/-- `ValRingEquiv R S` is the type of ring isomorphisms that preserves valuation from valued ring `R` to valued ring `S`. - -When possible, instead of parametrizing results over `(f : ValRingEquiv R S)`, -you should parametrize over `(F : Type*) [ValRingEquivClass F R S] (f : F)`. - -When you extend this structure, make sure to extend `ValRingEquivClass`. --/ -structure ValRingEquiv (R S : Type*) {ΓR ΓS : outParam Type*} [Ring R] [Ring S] - [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓS] - [vR : Valued R ΓR] [vS : Valued S ΓS] - extends OrderRingIso R S, Homeomorph R S where - val_isEquiv_comap' : vR.v.IsEquiv (vS.v.comap toRingEquiv) - -/-- Reinterpret a valued ring isomorphism into a ordered ring isomorphism. -/ -add_decl_doc ValRingEquiv.toOrderRingIso - -attribute [coe] ValRingEquiv.toOrderRingIso - -@[inherit_doc] -infixr:25 " ≃+*v " => ValRingEquiv - -end Hom - -section Class - -/-- `ValHomClass F R S` asserts that `F` is a type of valuation-preserving morphisms. -/ -class ValRingHomClass (F R S : Type*) {ΓR ΓS : outParam Type*} [Ring R] [Ring S] - [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓS] - [vR : Valued R ΓR] [vS : Valued S ΓS] [FunLike F R S] extends RelHomClass F ((· ≤ ·) : R → R → Prop) ((· ≤ ·) : S → S → Prop), RingHomClass F R S, ContinuousMapClass F R S : Prop where - val_isEquiv_comap (f : F) : vR.v.IsEquiv (vS.v.comap f) - -export ValRingHomClass (val_isEquiv_comap) - -class ValRingEquivClass (F R S : Type*) {ΓR ΓS : outParam Type*} [Ring R] [Ring S] - [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓS] - [vR : Valued R ΓR] [vS : Valued S ΓS] [EquivLike F R S] extends OrderIsoClass F R S, RingEquivClass F R S, ContinuousMapClass F R S : Prop where - inv_continuous (f : F) : Continuous (EquivLike.inv f) - val_isEquiv_comap (f : F) : vR.v.IsEquiv (vS.v.comap f) - -variable {F R S : Type*} {ΓR ΓS : outParam Type*} [Ring R] [Ring S] - [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓS] - [vR : Valued R ΓR] [vS : Valued S ΓS] - -/-- Turn an element of a type `F` satisfying `ValRingHomClass F R S` into an actual -`ValRingHom`. This is declared as the default coercion from `F` to `R →+*v S`. -/ -@[coe] -def ValRingHomClass.toValRingHom [FunLike F R S] [ValRingHomClass F R S] (f : F) : - R →+*v S := - { OrderHomClass.toOrderHom f, RingHomClass.toRingHom f, toContinuousMap f with val_isEquiv_comap' := ValRingHomClass.val_isEquiv_comap f} - -/-- Any type satisfying `ValRingHomClass` can be cast into `ValRingHom` via -`ValRingHomClass.toValRingHom`. -/ -instance [FunLike F R S] [ValRingHomClass F R S] : CoeTC F (R →+*v S) := - ⟨ValRingHomClass.toValRingHom⟩ - -/-- Turn an element of a type `F` satisfying `ValRingEquivClass F R S` into an actual -`ValRingEquiv`. This is declared as the default coercion from `F` to `R ≃+*v S`. -/ -@[coe] -def ValRingEquivClass.toValRingEquiv [EquivLike F R S] [ValRingEquivClass F R S] (f : F) : - R ≃+*v S := - { OrderIsoClass.toOrderIso f, RingEquivClass.toRingEquiv f, toContinuousMap f with - val_isEquiv_comap' := ValRingEquivClass.val_isEquiv_comap f - map_le_map_iff' := map_le_map_iff f - continuous_invFun := ValRingEquivClass.inv_continuous f - } - -/-- Any type satisfying `ValRingHomClass` can be cast into `ValRingHom` via -`ValRingHomClass.toValRingHom`. -/ -instance [FunLike F R S] [ValRingHomClass F R S] : CoeTC F (R →+*v S) := - ⟨ValRingHomClass.toValRingHom⟩ - -/-- Any type satisfying `ValRingEquivClass` can be cast into `ValRingEquiv` via -`ValRingEquivClass.toValRingEquiv`. -/ -instance [EquivLike F R S] [ValRingEquivClass F R S] : CoeTC F (R ≃+*v S) := - ⟨ValRingEquivClass.toValRingEquiv⟩ - --- See note [lower instance priority] -instance (priority := 100) ValRingEquivClass.toValRingHomClass - [EquivLike F R S] [ValRingEquivClass F R S] : ValRingHomClass F R S := - { OrderIsoClass.toOrderHomClass with - val_isEquiv_comap := ValRingEquivClass.val_isEquiv_comap } - -section Hom - -variable [FunLike F R S] [ValRingHomClass F R S] - -@[simp] -theorem val_map_le_iff (f : F) {x y : R} : v (f x) ≤ v (f y) ↔ v x ≤ v y := (val_isEquiv_comap f x y).symm - -@[simp] -theorem val_map_lt_iff (f : F) {x y : R} : v (f x) < v (f y) ↔ v x < v y := by - convert (val_map_le_iff f).not <;> - push_neg <;> rfl - -@[simp] -theorem val_map_le_one_iff (f : F) {x : R} : v (f x) ≤ 1 ↔ v x ≤ 1 := by - convert val_map_le_iff f (x := x) (y := 1) <;> - simp only [_root_.map_one] - -@[simp] -theorem val_map_lt_one_iff (f : F) {x : R} : v (f x) < 1 ↔ v x < 1 := by - convert val_map_lt_iff f (x := x) (y := 1) <;> - simp only [_root_.map_one] - -end Hom - -section Equiv - -variable [EquivLike F R S] [ValRingEquivClass F R S] - -@[simp] -theorem val_map_inv_le_val_iff (f : F) {x : R} {y : S} : v (EquivLike.inv f y) ≤ v x ↔ v y ≤ v (f x) := by - convert (val_map_le_iff f).symm - exact (EquivLike.right_inv f _).symm - -@[simp] -theorem val_le_val_map_inv_iff (f : F) {x : R} {y : S} : v x ≤ v (EquivLike.inv f y) ↔ v (f x) ≤ v y := by - convert (val_map_le_iff f).symm - exact (EquivLike.right_inv _ _).symm - -@[simp] -theorem val_map_inv_lt_val_iff (f : F) {x : R} {y : S} : v (EquivLike.inv f y) < v x ↔ v y < v (f x) := by - convert (val_le_val_map_inv_iff f (x := x) (y := y)).not <;> - push_neg <;> rfl - -@[simp] -theorem val_lt_val_map_inv_iff (f : F) {x : R} {y : S} : v x < v (EquivLike.inv f y) ↔ v (f x) < v y := by - convert (val_map_inv_le_val_iff f (x := x) (y := y)).not <;> - push_neg <;> rfl - -end Equiv - -end Class - -variable {R S T: Type*} {ΓR ΓS ΓT : outParam Type*} - [Ring R] [Ring S] [Ring T] - [LinearOrderedCommGroupWithZero ΓR] - [LinearOrderedCommGroupWithZero ΓS] - [LinearOrderedCommGroupWithZero ΓT] - [vR : Valued R ΓR] [vS : Valued S ΓS] [vT : Valued T ΓT] - -section HomIsClass - -instance : FunLike (ValRingHom R S) R S where - coe f := f.toFun - coe_injective' f g h := by - rcases f with ⟨⟨_, _⟩, _⟩ - rcases g with ⟨⟨_, _⟩, _⟩ - dsimp at h - congr - apply DFunLike.coe_injective' h - -instance : ValRingHomClass (ValRingHom R S) R S where - map_rel f _ _ h:= f.monotone' h - map_mul f := f.map_mul - map_one f := f.map_one - map_add f := f.map_add - map_zero f := f.map_zero - map_continuous f := f.toContinuousMap.continuous_toFun - val_isEquiv_comap f := f.val_isEquiv_comap' - -instance : EquivLike (ValRingEquiv R S) R S where - coe f := f.toFun - inv f := f.invFun - left_inv f := f.left_inv - right_inv f := f.right_inv - coe_injective' f g h _ := by - rcases f with ⟨⟨_, _⟩, _⟩ - rcases g with ⟨⟨_, _⟩, _⟩ - dsimp at h - congr - apply DFunLike.coe_injective' h - -instance : ValRingEquivClass (ValRingEquiv R S) R S where - map_le_map_iff f := f.map_le_map_iff' - map_mul f := f.map_mul - map_add f := f.map_add - map_continuous f := f.toHomeomorph.continuous_toFun - inv_continuous f := f.toHomeomorph.continuous_invFun - val_isEquiv_comap f := f.val_isEquiv_comap' - -end HomIsClass - -section coe_and_lemma - --- `How should one organize coe lemmas???` -namespace ValRingHom - --- theorem val_isEquiv_comap (R S : Type*) {ΓR ΓS : outParam Type*} [Ring R] [Ring S] --- [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓS] --- [vR : Valued R ΓR] [vS : Valued S ΓS] (f : R →+*v S) : vR.v.IsEquiv (vS.v.comap f) := f.val_isEquiv_comap' - --- @[simp] --- theorem toOrderRingHom_eq_coe (f : R →+*v S) : f.toOrderRingHom = f := rfl - --- @[simp] --- theorem toFun_eq_coe (f : R →+*v S) : f.toFun = f := rfl - -@[ext] -theorem ext {f g : R →+*v S} (h : (f : R → S) = g) : f = g := DFunLike.coe_injective h - --- @[simp] --- theorem coe_eq (f : R →+*v S) : ValRingHomClass.toValRingHom f = f := rfl - -end ValRingHom - --- @[simp] --- theorem ValRingHomClass.coe_coe {F} [FunLike F R S] [ValRingHomClass F R S] (f : F) : ⇑(f : R →+*v S) = f := rfl - --- @[simp] --- theorem ValRingHomClass.coe_toOrderRingIso {F} [FunLike F R S] [ValRingHomClass F R S] (f : F) : ⇑(f : R →+*o S) = f := rfl - -namespace ValRingEquiv - --- @[simp] --- theorem toFun_eq_coe (f : R ≃+*v S) : f.toFun = f := rfl - --- @[simp] --- theorem toRingEquiv_toOrderRingIso_eq_coe (f : R ≃+*v S) : ((f.toOrderRingIso) : R ≃+* S) = f := rfl - --- @[simp] --- theorem coe_toOrderRingIso_eq_coe (f : R ≃+*v S) : ⇑(f.toOrderRingIso) = f := rfl - -@[ext] -theorem ext (f g : R ≃+*v S) (h : (f : R → S) = g) : f = g := DFunLike.coe_injective h - -theorem bijective (f : R ≃+*v S) : Function.Bijective f := f.toEquiv.bijective - -theorem injective (f : R ≃+*v S) : Function.Injective f := f.toEquiv.injective - -theorem surjective (f : R ≃+*v S) : Function.Surjective f := f.toEquiv.surjective - --- @[simp] --- theorem coe_eq (f : R ≃+*v S) : ValRingEquivClass.toValRingEquiv f = f := rfl - -end ValRingEquiv - --- @[simp] --- theorem ValRingEquivClass.coe_coe {F} [EquivLike F R S] [ValRingEquivClass F R S] (f : F) : ⇑(f : R ≃+*v S) = f := rfl - --- @[simp] --- theorem ValRingEquivClass.coe_toOrderRingIso {F} [EquivLike F R S] [ValRingEquivClass F R S] (f : F) : ⇑(f : R ≃+*o S) = f := rfl - -/- ` Add these ` -Low TODO : canlift - -Low TODO :coe simp lemmas, such as - -toOrderRingIso coe_mk coe_mk' toFun_eq_coe - -How should these coe lemma be organized?? - -`refl symm trans group` --/ - -end coe_and_lemma - -section mk' - -theorem map_le_map_iff_of_val_isEquiv_comap {f : R ≃+* S} {x y : R} (hf : vR.v.IsEquiv (vS.v.comap f)) : f x ≤ f y ↔ x ≤ y := by - rw [le_iff_val_le, le_iff_val_le] - exact (hf x y).symm - -theorem monotone_of_val_isEquiv_comap {f : R →+* S} (hf : vR.v.IsEquiv (vS.v.comap f)) : Monotone f := by - intro x y h - rw [le_iff_val_le] at h ⊢ - exact (hf x y).1 h - --- to Mathlib Mathlib.Topology.Algebra.Valuation -theorem Valued.mem_nhds' {R : Type*} [Ring R] {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] {s : Set R} {x : R} : -s ∈ nhds x ↔ ∃ (a : R), Valued.v a > 0 ∧ {y : R | Valued.v (y - x) < Valued.v a} ⊆ s := sorry - -theorem continuous_of_val_isEquiv_comap {f : R →+* S} (hf : vR.v.IsEquiv (vS.v.comap f)) : Continuous f := by - rw [continuous_iff_continuousAt] - intro x - simp [ContinuousAt, Filter.Tendsto, Filter.map] - intro s - simp - rw [Valued.mem_nhds', Valued.mem_nhds'] - rintro ⟨a, ⟨ha, h⟩⟩ - -- use a - sorry -- difficult - --- lower TODO : stronger version, f is topological embedding - -protected theorem val_isEquiv_comap.symm {f : R ≃+* S} (hf : vR.v.IsEquiv (vS.v.comap f)) : vS.v.IsEquiv (vR.v.comap f.symm) := by - intro x y - convert (hf (f.invFun x) (f.invFun y)).symm <;> - simp only [RingEquiv.toEquiv_eq_coe, Equiv.invFun_as_coe, comap_apply, RingHom.coe_coe, - EquivLike.apply_coe_symm_apply] - -def ValRingHom.mk' {f : R →+* S} (hf : vR.v.IsEquiv (vS.v.comap f)) : R →+*v S where - toRingHom := f - monotone' := monotone_of_val_isEquiv_comap hf - val_isEquiv_comap' := hf - continuous_toFun := continuous_of_val_isEquiv_comap hf - -def ValRingEquiv.mk' {f : R ≃+* S} (hf : vR.v.IsEquiv (vS.v.comap f)) : R ≃+*v S where - toRingEquiv := f - map_le_map_iff' := map_le_map_iff_of_val_isEquiv_comap hf - continuous_toFun := continuous_of_val_isEquiv_comap hf - continuous_invFun := continuous_of_val_isEquiv_comap (val_isEquiv_comap.symm hf) - val_isEquiv_comap' := hf - --- TODO: coe lemmas of mk', @[simp] - -end mk' - -section Composition - -namespace ValRingHom - -variable (R) in -/-- The identity function as bundled valuation ring homomorphism. -/ -def id : R →+*v R := - ⟨.id R, continuous_id , IsEquiv.refl⟩ - -instance : Inhabited (R →+*v R) := ⟨ ValRingHom.id R ⟩ - -@[simp] -theorem id_apply (r : R) : ValRingHom.id R r = r := rfl - -def comp (g : S →+*v T) (f : R →+*v S) : R →+*v T where - toOrderRingHom := (↑g : OrderRingHom S T).comp f - continuous_toFun := by - simp only [OrderRingHom.comp] - dsimp - exact Continuous.comp g.continuous_toFun f.continuous_toFun - val_isEquiv_comap' := by - intro x y - convert f.val_isEquiv_comap' x y - exact (g.val_isEquiv_comap' (f x) (f y)).symm - -@[simp] -theorem id_comp (f : R →+*v S) : (ValRingHom.id S).comp f = f := by - ext - rfl - -@[simp] -theorem comp_id (f : R →+*v S) : f.comp (.id R) = f := by - ext - rfl - -end ValRingHom - -namespace ValRingEquiv - -variable (R) in -/-- Identity valued ring isomorphism. -/ -@[refl] -def refl : (R ≃+*v R) where - toOrderRingIso := .refl R - continuous_toFun := continuous_id - continuous_invFun := continuous_id - val_isEquiv_comap' := IsEquiv.refl - -@[simp] -theorem coe_refl : (refl R : R →+*v R) = .id R := - rfl - -@[simp] -theorem refl_apply (x : R) : refl R x = x := - rfl - -@[simp] -theorem refl_toEquiv : (refl R).toEquiv = Equiv.refl R := - rfl - -/-- Inverse of an valued ring isomorphism. -/ -def symm (f : R ≃+*v S) : S ≃+*v R where - toOrderRingIso := OrderRingIso.symm f - continuous_toFun := f.continuous_invFun - continuous_invFun := f.continuous_toFun - val_isEquiv_comap' := by - intro x y - convert IsEquiv.symm (val_isEquiv_comap f) (f.invFun x) (f.invFun y) <;> - simp only [comap_apply] <;> - congr <;> - exact (f.right_inv _).symm - -@[simp] -theorem apply_symm_apply (f : R ≃+*v S) (x : S) : f (f.symm x) = x := - f.toEquiv.apply_symm_apply x - -@[simp] -theorem symm_apply_apply (f : R ≃+*v S) (x : R) : f.symm (f x) = x := - f.toEquiv.symm_apply_apply x - -@[simp] -theorem symm_refl : (ValRingEquiv.refl R).symm = .refl R := rfl - -theorem apply_eq_iff_eq_symm_apply (f : R ≃+*v S) (x : R) (y : S) : f x = y ↔ x = f.symm y := - f.toEquiv.apply_eq_iff_eq_symm_apply - -theorem symm_apply_eq (f : R ≃+*v S) {x : R} {y : S} : f.symm y = x ↔ y = f x := - f.toEquiv.symm_apply_eq - -@[simp] -theorem symm_symm (f : R ≃+*v S) : f.symm.symm = f := rfl - -theorem symm_bijective : Function.Bijective (.symm : (R ≃+*v S) → S ≃+*v R) := - Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩ - -theorem symm_injective : Function.Injective (.symm : (R ≃+*v S) → S ≃+*v R) := - symm_bijective.injective - -theorem symm_surjective : Function.Surjective (.symm : (R ≃+*v S) → S ≃+*v R) := - symm_bijective.surjective - -@[simp] -theorem toEquiv_symm (f : R ≃+*v S) : f.toEquiv.symm = f.symm.toEquiv := - rfl - -/-- Composition of two valued ring isomorphisms is an order isomorphism. -/ -@[trans] -def trans (f : R ≃+*v S) (f' : S ≃+*v T) : R ≃+*v T where -- trans has different order comparing with comp - toOrderRingIso := OrderRingIso.trans (β := S) f f' - continuous_toFun := by - apply Continuous.comp (Y := S) - exact f'.continuous_toFun - exact f.continuous_toFun - continuous_invFun := by - apply Continuous.comp (Y := S) - exact f.continuous_invFun - exact f'.continuous_invFun - val_isEquiv_comap' := by - intro x y - convert f.val_isEquiv_comap' x y - exact (f'.val_isEquiv_comap' (f x) (f y)).symm - -@[simp] -theorem coe_trans (e : R ≃+*v S) (e' : S ≃+*v T) : ⇑(e.trans e') = e' ∘ e := - rfl - -@[simp] -theorem trans_apply (e : R ≃+*v S) (e' : S ≃+*v T) (x : R) : e.trans e' x = e' (e x) := - rfl - -@[simp] -theorem refl_trans (e : R ≃+*v S) : (refl R).trans e = e := by - ext x - rfl - -@[simp] -theorem trans_refl (e : R ≃+*v S) : e.trans (refl S) = e := by - ext x - rfl - -@[simp] -theorem symm_trans_apply (e₁ : R ≃+*v S) (e₂ : S ≃+*v T) (c : T) : - (e₁.trans e₂).symm c = e₁.symm (e₂.symm c) := - rfl - -theorem symm_trans (e₁ : R ≃+*v S) (e₂ : S ≃+*v T) : (e₁.trans e₂).symm = e₂.symm.trans e₁.symm := - rfl - -@[simp] -theorem symm_trans_self (e : R ≃+*v S) : e.trans e.symm = .refl R := by - ext; apply Equiv.left_inv - -@[simp] -theorem self_symm_trans (e : R ≃+*v S) : e.symm.trans e = .refl S := by - ext; apply Equiv.right_inv - --- -- structures on ValRingIso -instance group : Group (R ≃+*v R) where - mul e e' := e'.trans e - mul_assoc := by intros; rfl - one := .refl R - one_mul := by intros; rfl - mul_one := by intros; rfl - inv := .symm - mul_left_inv := symm_trans_self - -@[simp] -theorem one_apply (x : R) : (1 : R ≃+*v R) x = x := rfl - -@[simp] -theorem mul_apply (e e' : (R ≃+*v R)) (x : R) : (e * e') x = e (e' x) := rfl - -end ValRingEquiv - -end Composition - -end ValRingHom_ValRingEquiv - -section ValAlgebra - -/-- A valued algebra over a valued commutative ring `R`, is a valued ring `A` together with a ring map into the center of `A` that preserves the valuation.-/ -class ValAlgebra (R A : Type*) {ΓR ΓA : outParam Type*} [CommRing R] [Ring A] [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] [vR : Valued R ΓR] [vA : Valued A ΓA] extends ValRingHom R A, Algebra R A - -/-- The valued ring homomorphism `R →+*v A` given by `Algebra` structure. -/ -def valAlgebraMap (R A : Type*) {ΓR ΓA : outParam Type*} [CommRing R] [Ring A] [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] [Valued R ΓR] [Valued A ΓA] [ValAlgebra R A] : R →+*v A := ValAlgebra.toValRingHom - -variable {R A : Type*} {ΓR ΓA : outParam Type*} [CommRing R] [Ring A] [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] [vR : Valued R ΓR] [vA : Valued A ΓA] [ValAlgebra R A] - --- Please do not use this in general, it has definitional equal problems. -/-- Creating a valued algebra from a valued ring morphism. -/ -def ValRingHom.toValAlgebra' (f : R →+*v A) (h : ∀ (c : R) (x : A), f c * x = x * f c): ValAlgebra R A where - toValRingHom := f - smul := (f.toAlgebra' h).smul - smul_def' := (f.toAlgebra' h).smul_def' - commutes' := (f.toAlgebra' h).commutes' - -def ValRingHom.toValAlgebra {R A : Type*} {ΓR ΓA : outParam Type*} [CommRing R] [CommRing A] [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] [Valued R ΓR] [Valued A ΓA] (f : R →+*v A) : ValAlgebra R A := - f.toValAlgebra' (fun _ => mul_comm _) - -theorem ValRingHom.valAlgebraMap_toValAlgebra {R A : Type*} {ΓR ΓA : outParam Type*} [CommRing R] [CommRing A] [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] [Valued R ΓR] [Valued A ΓA] [ValAlgebra R A] (f : R →+*v A) : - @valAlgebraMap R A _ _ _ _ _ _ _ _ f.toValAlgebra = f := - rfl - -namespace ValAlgebra - -/-- To prove two valued algebra structures on a fixed `[CommRing R] [Ring A]` agree, -it suffices to check the `algebraMap`s agree. --/ -@[ext] -theorem valAlgebra_ext (P Q : ValAlgebra R A) - (h : ∀ r : R, (haveI := P; valAlgebraMap R A r) = haveI := Q; valAlgebraMap R A r) : - P = Q := by - replace h : P.toRingHom = Q.toRingHom := DFunLike.ext _ _ h - have h' : (haveI := P; (· • ·) : R → A → A) = (haveI := Q; (· • ·) : R → A → A) := by - funext r a - rw [P.smul_def', Q.smul_def', h] - rcases P with @⟨⟨⟨P⟩⟩, ⟨PSmul⟩⟩ - rcases Q with @⟨⟨⟨Q⟩⟩, ⟨QSmul⟩⟩ - congr - -theorem val_isEquiv_comap : vR.v.IsEquiv (vA.v.comap (algebraMap R A)) := - (valAlgebraMap R A).val_isEquiv_comap' - -open algebraMap - -@[simp] -theorem val_map_le_iff (x y : R) : v (x : A) ≤ v (y : A) ↔ v x ≤ v y := - _root_.val_map_le_iff (valAlgebraMap R A) - -@[simp] -theorem val_map_lt_iff (x y : R) : v (x : A) < v (y : A) ↔ v x < v y := - _root_.val_map_lt_iff (valAlgebraMap R A) - -@[simp] -theorem val_map_le_one_iff (x : R) : v (x : A) ≤ 1 ↔ v x ≤ 1 := - _root_.val_map_le_one_iff (valAlgebraMap R A) - -@[simp] -theorem val_map_lt_one_iff (x : R) : v (x : A) < 1 ↔ v x < 1 := - _root_.val_map_lt_one_iff (valAlgebraMap R A) - -variable (R) in -/-- The identity map inducing an `ValAlgebra` structure. -/ -instance id : ValAlgebra R R where - -- copied from `Algebra.id` - -- We override `toFun` and `toSMul` because `ValRingHom.id` is not reducible and cannot - -- be made so without a significant performance hit. - -- see library note [reducible non-instances]. - toFun x := x - toSMul := Mul.toSMul _ - __ := ValRingHom.toValAlgebra (ValRingHom.id R) - -namespace id - -@[simp] -theorem map_eq_id : valAlgebraMap R R = ValRingHom.id R := - rfl - -theorem map_eq_self (x : R) : valAlgebraMap R R x = x := - rfl - -end id - -end ValAlgebra - -end ValAlgebra - -section ValAlgHom_ValAlgEquiv - -section Hom - -variable (R A B : Type*) [CommRing R] [Ring A] [Ring B] {ΓR ΓA ΓB : outParam Type*} [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] [LinearOrderedCommGroupWithZero ΓB] [Valued R ΓR] [vA : Valued A ΓA] [vB : Valued B ΓB] [ValAlgebra R A] [ValAlgebra R B] - -/-- Defining the homomorphism in the category of valued-`R`-algebra. -/ -structure ValAlgHom extends ValRingHom A B, AlgHom R A B - -/-- Defining the isomorphism in the category of valued-`R`-algebra. -/ -structure ValAlgEquiv extends ValRingEquiv A B, AlgEquiv R A B - -/-- Reinterpret an `ValAlgHom` as a `ValRingHom` -/ -add_decl_doc ValAlgHom.toValRingHom -attribute [coe] ValAlgHom.toValRingHom - -/-- Reinterpret an `ValAlgHom` as a `AlgHom` -/ -add_decl_doc ValAlgHom.toAlgHom -attribute [coe] ValAlgHom.toAlgHom - -/-- Reinterpret an `ValAlgEquiv` as a `ValRingEquiv` -/ -add_decl_doc ValAlgEquiv.toValRingEquiv -attribute [coe] ValAlgEquiv.toValRingEquiv - -/-- Reinterpret an `ValAlgEquiv` as a `AlgEquiv` -/ -add_decl_doc ValAlgEquiv.toAlgEquiv -attribute [coe] ValAlgEquiv.toAlgEquiv - -@[inherit_doc] -notation:25 A " →ₐv[" R "] " B => ValAlgHom R A B - -@[inherit_doc] -notation:25 A " ≃ₐv[" R "] " B => ValAlgEquiv R A B - -end Hom - -variable {R A B C D: Type*} [CommRing R] [Ring A] [Ring B] [Ring C] [Ring D] -{ΓR ΓA ΓB ΓC ΓD: outParam Type*} [LinearOrderedCommGroupWithZero ΓR] -[LinearOrderedCommGroupWithZero ΓA] [LinearOrderedCommGroupWithZero ΓB] -[LinearOrderedCommGroupWithZero ΓC] -[LinearOrderedCommGroupWithZero ΓD] -[Valued R ΓR] [vA : Valued A ΓA] [vB : Valued B ΓB] [vC : Valued C ΓC] [vD : Valued D ΓD] -[fA : ValAlgebra R A] [fB : ValAlgebra R B] [fC : ValAlgebra R C] [fD : ValAlgebra R D] - -section Class - -/-- `ValAlgHomClass F R A B` asserts `F` is a type of bundled valued algebra homomorphisms -from `A` to `B`. -/ -class ValAlgHomClass (F : Type*) (R A B : outParam Type*) [CommRing R] [Ring A] [Ring B] - {ΓR ΓA ΓB : outParam Type*} [LinearOrderedCommGroupWithZero ΓR] - [LinearOrderedCommGroupWithZero ΓA] [LinearOrderedCommGroupWithZero ΓB] - [Valued R ΓR] [vA : Valued A ΓA] [vB : Valued B ΓB] [ValAlgebra R A] [ValAlgebra R B] - [FunLike F A B] extends ValRingHomClass F A B, AlgHomClass F R A B : Prop - -instance : FunLike (A →ₐv[R] B) A B where - coe f := f.toFun - coe_injective' f g h := by - rcases f with ⟨⟨_, _⟩, _⟩ - rcases g with ⟨⟨_, _⟩, _⟩ - dsimp at h - congr - apply DFunLike.coe_injective' - exact h - -instance : EquivLike (A ≃ₐv[R] B) A B where - coe f := f.toFun - inv f := f.invFun - left_inv f := f.left_inv - right_inv f := f.right_inv - coe_injective' f g h _ := by - rcases f with ⟨⟨_, _⟩, _⟩ - rcases g with ⟨⟨_, _⟩, _⟩ - dsimp at h - congr - apply DFunLike.coe_injective' - exact h - -instance (priority := 100) : ValRingHomClass (A →ₐv[R] B) A B where - map_rel f := map_rel f.toValRingHom - map_mul f := f.map_mul - map_one f := f.map_one - map_add f := f.map_add - map_zero f := f.map_zero - map_continuous f := f.toValRingHom.continuous_toFun - val_isEquiv_comap f := f.val_isEquiv_comap' - -instance (priority := 100) : ValRingEquivClass (A ≃ₐv[R] B) A B where - map_le_map_iff f := map_le_map_iff f.toValRingEquiv - map_mul f := f.map_mul - map_add f := f.map_add - map_continuous f := f.toValRingEquiv.continuous_toFun - inv_continuous f := f.toValRingEquiv.continuous_invFun - val_isEquiv_comap f := f.val_isEquiv_comap' - -instance (priority := 100) : AlgHomClass (A →ₐv[R] B) R A B := -{ - commutes := fun f => f.commutes' -} - -instance (priority := 100) : AlgEquivClass (A ≃ₐv[R] B) R A B := -{ - commutes := fun f => f.commutes' -} - -@[coe] -def ValAlgHom.ofAlgHomClassValRingHomClass {F : Type*} - [FunLike F A B] [ValRingHomClass F A B] [AlgHomClass F R A B] (f : F) : - A →ₐv[R] B := - { ValRingHomClass.toValRingHom f, AlgHomClass.toAlgHom f with} - -instance (priority := 100) {F : Type*} - [FunLike F A B] [ValRingHomClass F A B] [AlgHomClass F R A B] : - CoeTC F (A →ₐv[R] B) where - coe := ValAlgHom.ofAlgHomClassValRingHomClass - -end Class - -section coe - -namespace ValAlgHom --- copy AlgHom.coe_coe, ... --- ..., coe_fn_injective - -@[ext] -theorem ext {f g : A →ₐv[R] B} (h : (f : A → B) = g) : f = g := DFunLike.coe_injective h - -end ValAlgHom - -theorem comp_valAlgebraMap {F} [FunLike F A B] [FunLike F A B] [ValRingHomClass F A B] [AlgHomClass F R A B] (φ : F) : (φ : A →+*v B).comp (valAlgebraMap R A) = valAlgebraMap R B := - DFunLike.ext _ _ <| AlgHomClass.commutes φ - -namespace ValAlgEquiv - -@[ext] -theorem ext {f g : A ≃ₐv[R] B} (h : ∀ a, f a = g a) : f = g := - DFunLike.ext f g h - -end ValAlgEquiv - -end coe - -namespace ValAlgHom - -def mk' (f : A →ₐ[R] B) (h : vA.v.IsEquiv (vB.v.comap f)) : A →ₐv[R] B where - toFun := f - map_one' := f.map_one - map_mul' := f.map_mul - map_zero' := f.map_zero - map_add' := f.map_add' - monotone' := monotone_of_val_isEquiv_comap h - val_isEquiv_comap' := h - commutes' := f.commutes' - continuous_toFun := continuous_of_val_isEquiv_comap h - -theorem coe_mk' (f : A →ₐ[R] B) (h : vA.v.IsEquiv (vB.v.comap f)) : (mk' f h) = f := rfl - --- def mk'' : given ValRingHom and commute. --- theorem coe_mk'' - -variable (R A) in -/-- Identity map as an `ValAlgHom`. -/ -protected def id : (A →ₐv[R] A) where - toOrderRingHom := .id A - continuous_toFun := continuous_id - val_isEquiv_comap' := IsEquiv.refl - commutes' _ := rfl - -@[simp] -theorem coe_id : ⇑(ValAlgHom.id R A) = id := - rfl - -@[simp] -theorem id_toValRingHom : (ValAlgHom.id R A : A →+* A) = ValRingHom.id A := - rfl - -@[simp] -theorem id_apply (p : A) : ValAlgHom.id R A p = p := - rfl - -protected def comp (φ₁ : B →ₐv[R] C) (φ₂ : A →ₐv[R] B) : A →ₐv[R] C := - { φ₁.toValRingHom.comp ↑φ₂ with - commutes' := fun r : R => by rw [← (φ₁ : B →ₐ[R] C).commutes', ← (φ₂ : A →ₐ[R] B).commutes]; rfl } - -@[simp] -theorem coe_comp (φ₁ : B →ₐv[R] C) (φ₂ : A →ₐv[R] B) : ⇑(φ₁.comp φ₂) = φ₁ ∘ φ₂ := - rfl - -theorem comp_apply (φ₁ : B →ₐv[R] C) (φ₂ : A →ₐv[R] B) (p : A) : φ₁.comp φ₂ p = φ₁ (φ₂ p) := - rfl - -theorem comp_toRingHom (φ₁ : B →ₐv[R] C) (φ₂ : A →ₐv[R] B) : - (φ₁.comp φ₂ : A →+*v C) = (φ₁ : B →+*v C).comp ↑φ₂ := - rfl - -@[simp] -theorem comp_id (φ : A →ₐv[R] B) : φ.comp (ValAlgHom.id R A) = φ := by - ext - rfl - -@[simp] -theorem id_comp (φ : A →ₐv[R] B) : (ValAlgHom.id R B).comp φ = φ := by - ext - rfl - -theorem comp_assoc (φ₁ : C →ₐv[R] D) (φ₂ : B →ₐv[R] C) (φ₃ : A →ₐv[R] B) : - (φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃) := by - ext - rfl - --- instance : Monoid (A →ₐv[R] A) - --- /-- `AlgebraMap` as an `AlgHom`. -/ --- def ofId : R →ₐv[R] A := - -end ValAlgHom - -namespace ValAlgEquiv - -def mk' (f : A ≃ₐ[R] B) (h : vA.v.IsEquiv (vB.v.comap f)) : A ≃ₐv[R] B := - { f, ValRingEquiv.mk' h with - commutes' := f.commutes' - } -theorem coe_mk' (f : A ≃ₐ[R] B) (h : vA.v.IsEquiv (vB.v.comap f)) : (mk' f h) = f := rfl - -@[refl] -def refl : (A ≃ₐv[R] A) where - toValRingEquiv := .refl A - commutes' _ := rfl - -instance : Inhabited (A ≃ₐv[R] A) := - ⟨.refl⟩ - -@[simp] -theorem refl_toAlgHom : ↑(.refl : A ≃ₐv[R] A) = AlgHom.id R A := - rfl - -@[simp] -theorem coe_refl : ⇑(.refl : A ≃ₐv[R] A) = id := - rfl - -/-- Inverse of a valued ring algebra equivalence. -/ -@[symm] -def symm (e : A ≃ₐv[R] B) : B ≃ₐv[R] A := - { e.toValRingEquiv.symm with - commutes' := fun r => by - rw [← e.toRingEquiv.symm_apply_apply (algebraMap R A r)] - congr - change _ = e _ - exact ((e : A →ₐ[R] B).commutes r).symm } - - -@[simp] -theorem symm_toEquiv_eq_symm {e : A ≃ₐv[R] B} : (e : A ≃ B).symm = e.symm := - rfl - -theorem invFun_eq_symm {e : A ≃ₐv[R] B} : e.invFun = e.symm := - rfl - -@[simp] -theorem symm_symm (e : A ≃ₐv[R] B) : e.symm.symm = e := by - ext - rfl - -theorem symm_bijective : Function.Bijective (symm : (A ≃ₐv[R] B) → B ≃ₐv[R] A) := - Function.bijective_iff_has_inverse.mpr ⟨_ , symm_symm, symm_symm⟩ - - -@[simp] -theorem refl_symm : (.refl : A ≃ₐv[R] A).symm = .refl := - rfl - -@[simp] -theorem toRingEquiv_symm (f : A ≃ₐv[R] A) : (f : A ≃+*v A).symm = f.symm := - rfl - -@[simp] -theorem symm_toRingEquiv (e : A ≃ₐv[R] B): (e.symm : B ≃+*v A) = (e : A ≃+*v B).symm := - rfl - -/-- Algebra equivalences are transitive. -/ -@[trans] -def trans (e₁ : A ≃ₐv[R] B) (e₂ : B ≃ₐv[R] C) : A ≃ₐv[R] C := - { e₁.toValRingEquiv.trans e₂.toValRingEquiv with - commutes' := fun r => show e₂.toFun (e₁.toFun _) = _ by rw [e₁.commutes', e₂.commutes'] } - -@[simp] -theorem apply_symm_apply (e : A ≃ₐv[R] B) : ∀ x, e (e.symm x) = x := - e.toEquiv.apply_symm_apply - -@[simp] -theorem symm_apply_apply (e : A ≃ₐv[R] B) : ∀ x, e.symm (e x) = x := - e.toEquiv.symm_apply_apply - -@[simp] -theorem self_symm_trans (e : A ≃ₐv[R] B) : e.symm.trans e = .refl := by - ext x - exact e.apply_symm_apply x - -@[simp] -theorem symm_trans_self (e : A ≃ₐv[R] B) : e.trans e.symm = .refl := by - ext x - exact e.symm_apply_apply x - -@[simp] -theorem symm_trans_apply (e₁ : A ≃ₐv[R] B) (e₂ : B ≃ₐv[R] C) (x : C) : - (e₁.trans e₂).symm x = e₁.symm (e₂.symm x) := - rfl - -@[simp] -theorem coe_trans (e₁ : A ≃ₐv[R] B) (e₂ : B ≃ₐv[R] C) : ⇑(e₁.trans e₂) = e₂ ∘ e₁ := - rfl - -@[simp] -theorem trans_apply (e₁ : A ≃ₐv[R] B) (e₂ : B ≃ₐv[R] C) (x : A) : (e₁.trans e₂) x = e₂ (e₁ x) := - rfl - -@[simp] -theorem comp_symm (e : A ≃ₐv[R] B) : ValAlgHom.comp (e : A →ₐv[R] B) e.symm = ValAlgHom.id R B := by - ext - simp only [ValAlgHom.coe_comp, Function.comp_apply, ValAlgHom.id_apply] - exact apply_symm_apply e _ - -@[simp] -theorem symm_comp (e : A ≃ₐv[R] B) : ValAlgHom.comp ↑e.symm (e : A →ₐv[R] B) = ValAlgHom.id R A := by - ext - simp only [ValAlgHom.coe_comp, Function.comp_apply, ValAlgHom.id_apply] - exact symm_apply_apply e _ - -theorem leftInverse_symm (e : A ≃ₐv[R] B) : Function.LeftInverse e.symm e := - e.left_inv - -theorem rightInverse_symm (e : A ≃ₐv[R] B) : Function.RightInverse e.symm e := - e.right_inv - --- /-- Promotes a bijective valued algebra homomorphism to an algebra equivalence. -/ --- noncomputable def ofBijective (f : A →ₐv[R] B) (hf : Function.Bijective f) : A ≃ₐv[R] B := --- { ValRingEquiv.ofBijective (f : A →+*v B) hf, f with } - --- /-- If `A` is equivalent to `A'` and `B` is equivalent to `B'`, then the type of maps --- `A →ₐv[R] B` is equivalent to the type of maps `A' →ₐv[R] B'`. -/ --- @[simps apply] --- def arrowCongr (e₁ : A ≃ₐv[R] A') (e₂ : B ≃ₐv[R] B') : (A →ₐv[R] B) ≃ (A' →ₐv[R] B') - --- def equivCongr - -instance {R A : Type*} [CommRing R] [Ring A] {ΓR ΓA : outParam Type*} [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] [Valued R ΓR] [Valued A ΓA] [ValAlgebra R A] : Group (A ≃ₐv[R] A) where - mul e e' := e'.trans e - mul_assoc _ _ _:= rfl - one := .refl - one_mul _ := rfl - mul_one _ := rfl - inv := symm - mul_left_inv := symm_trans_self - -@[simp] -theorem one_apply (x : A) : (1 : A ≃ₐv[R] A) x = x := rfl - -@[simp] -theorem one_def : (1 : A ≃ₐv[R] A) = .refl := rfl - -@[simp] -theorem mul_apply (e e' : (A ≃ₐv[R] A)) (x : A) : (e * e') x = e (e' x) := rfl - --- bundled version of forgetful, this will be enhanced to a equiv in certain cases -def toAlgEquivₘ : (A ≃ₐv[R] A) →* (A ≃ₐ[R] A) where - toFun := ValAlgEquiv.toAlgEquiv (R := R) (A := A) (B := A) - map_one' := rfl - map_mul' _ _ := by - ext - rfl - -@[simp] -theorem toAlgEquivₘ_coe (f : A ≃ₐv[R] A) : toAlgEquivₘ f = (f : A → A) := by - ext - rfl - -theorem toAlgEquiv_injective : Function.Injective (toAlgEquivₘ : (A ≃ₐv[R] A) →* (A ≃ₐ[R] A)) := by - intro _ _ h - apply DFunLike.coe_injective - exact congrArg ((↑) : (A ≃ₐ[R] A) → A → A) h - -end ValAlgEquiv - -end ValAlgHom_ValAlgEquiv diff --git a/RamificationGroup/Unused/Valued/Hom/Discrete'.lean b/RamificationGroup/Unused/Valued/Hom/Discrete'.lean deleted file mode 100644 index 33a4637..0000000 --- a/RamificationGroup/Unused/Valued/Hom/Discrete'.lean +++ /dev/null @@ -1,49 +0,0 @@ -import RamificationGroup.Valued.Hom.ValExtension -import Mathlib.FieldTheory.IntermediateField -import LocalClassFieldTheory.DiscreteValuationRing.Extensions - -open Valuation Valued DiscreteValuation - --- an instance of Valued for intermediate field (??) --- two instance of IsValExtension for maria's valued, K to K' and K' to K'' - -namespace DiscreteValuation - -variable {K K' L : Type*} {ΓK ΓK' : outParam Type*} [Field K] [Field L] -[vK : Valued K ℤₘ₀] [CompleteSpace K] -[IsDiscrete vK.v] [Algebra K L] {K' K'' : IntermediateField K L} [FiniteDimensional K K'] [FiniteDimensional K K''] - --- `Maybe this is bad` -noncomputable scoped instance intermidateFieldValued : Valued K' ℤₘ₀ := DiscreteValuation.Extension.valued K K' - -scoped instance intermidateFieldIsValExtension : IsValExtension K K' where - val_isEquiv_comap := sorry - -scoped instance intermidateFieldIsDiscrete: IsDiscrete (DiscreteValuation.Extension.valued K K').v := DiscreteValuation.Extension.isDiscrete_of_finite K K' - -end DiscreteValuation - -/- -variable {K K' L : Type*} {ΓK ΓK' : outParam Type*} [Field K] [Field K'] [Field L] -[vK : Valued K ℤₘ₀] [vL : Valued L ℤₘ₀] -[IsDiscrete vK.v] [IsDiscrete vL.v] [Algebra K L] [IsValExtension K L] [FiniteDimensional K L] {K' : IntermediateField K L} - ---{H : Subgroup (L ≃ₐ[K] L)} [H.Normal] - -namespace DiscreteValuation --- should be in file talking about both Discrete and ValAlgHom, probably Hom.Discrete -scoped instance valuedIntermediateField : Valued K' ℤₘ₀ := sorry - -scoped instance : IsDiscrete ((valuedIntermediateField (K':= K')).v) := sorry - -#synth IsScalarTower K K' L - -#synth Algebra K' L - - -scoped instance : IsValExtension K' L := sorry -#synth Algebra K K' -scoped instance : IsValExtension K K' := sorry - -end DiscreteValuation --/ diff --git a/RamificationGroup/Unused/Valued/Hom/Lift.lean b/RamificationGroup/Unused/Valued/Hom/Lift.lean deleted file mode 100644 index 1fec97a..0000000 --- a/RamificationGroup/Unused/Valued/Hom/Lift.lean +++ /dev/null @@ -1,209 +0,0 @@ -import LocalClassFieldTheory.DiscreteValuationRing.Extensions -import RamificationGroup.Valued.Defs - -open DiscreteValuation Valuation Valued - -section check - -variable (K : Type*) [Field K] [hv : Valued K ℤₘ₀] - (L : Type u_1) [Field L] [Algebra K L] [IsDiscrete hv.v] [CompleteSpace K] - [FiniteDimensional K L] - -#check DiscreteValuation.Extension.integralClosure_eq_integer - -example : Subalgebra.toSubring (integralClosure (↥(Valuation.valuationSubring hv.v)) L) = - (valuationSubring (extendedValuation K L)).toSubring := DiscreteValuation.Extension.integralClosure_eq_integer _ _ - -#synth Algebra 𝒪[K] (integralClosure 𝒪[K] L) - --- #synth Algebra 𝒪[K] ((extendedValuation K L).valuationSubring) -- failed -end check - -namespace ValRingHom - -variable {R S : Type*} [Ring R] [Ring S] {ΓR ΓS: Type*} [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓS] [vR : Valued R ΓR] [vS : Valued S ΓS] - --- `valuation_subring.algebra` instance as algebra Maria and Phillip gives instance on K₀ and L₀ L₀ := valuationSubring of extended valuation -def liftInteger (f : R →+*v S) : vR.v.integer →+*v vS.v.integer where - toFun x := ⟨f x.val, sorry⟩ - map_one' := by ext; exact f.map_one - map_mul' _ _ := by ext; exact f.map_mul _ _ - map_zero' := by ext; exact f.map_zero - map_add' _ _ := by ext; exact f.map_add _ _ - monotone' := sorry -- a theorem saying O[K] to K is order preserving - continuous_toFun := sorry - val_isEquiv_comap' := sorry - -variable {K L : Type*} [Field K] [Field L] {ΓK ΓL: outParam Type*} [LinearOrderedCommGroupWithZero ΓK] [LinearOrderedCommGroupWithZero ΓL] [vK : Valued K ΓK] [vL : Valued L ΓL] [ValAlgebra K L] - -def liftValuationSubring (f : K →+*v L) : 𝒪[K] →+*v 𝒪[L] := f.liftInteger - -#synth LocalRing 𝒪[K] -#synth LocalRing 𝒪[L] - -instance liftValuationSubring.IsLocalRingHom {f : K →+*v L} : IsLocalRingHom (f.liftValuationSubring : 𝒪[K] →+* 𝒪[L]) := sorry - -def liftResidueField (f : K →+*v L) : 𝓀[K] →+* 𝓀[L] := LocalRing.ResidueField.map (f.liftValuationSubring) -- TODO? : Should residue field be equipped with trivial valuation and enhance this to a ValRingHom? - -variable (f : K →+*v L)(s : 𝒪[K] →+*v 𝒪[L]) -#check (s : 𝒪[K] →+* 𝒪[L]) -#check f.liftValuationSubring --- #synth IsLocalRingHom (liftValuationSubring f) --- #synth IsLocalRingHom (f.liftValuationSubring.toRingHom) -- coe is not def eq to .toRingHom -#check liftValuationSubring.IsLocalRingHom - -end ValRingHom - -namespace ValRingEquiv - -variable {R S : Type*} [Ring R] [Ring S] {ΓR ΓS: Type*} [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓS] [vR : Valued R ΓR] [vS : Valued S ΓS] - --- `valuation_subring.algebra` instance as algebra Maria and Phillip gives instance on K₀ and L₀ L₀ := valuationSubring of extended valuation -def liftInteger (f : R ≃+*v S) : vR.v.integer ≃+*v vS.v.integer where - toFun x := ⟨f x.val, sorry⟩ - invFun y := ⟨f.invFun y.val, sorry⟩ - left_inv _ := by ext; exact f.left_inv _ - right_inv _ := by ext; exact f.right_inv _ - map_mul' _ _ := by ext; exact f.map_mul' _ _ - map_add' _ _ := by ext; exact f.map_add' _ _ - map_le_map_iff' := sorry - continuous_toFun := sorry - continuous_invFun := sorry - val_isEquiv_comap' := sorry - - -variable {K L : Type*} [Field K] [Field L] {ΓK ΓL: outParam Type*} [LinearOrderedCommGroupWithZero ΓK] [LinearOrderedCommGroupWithZero ΓL] [vK : Valued K ΓK] [vL : Valued L ΓL] [ValAlgebra K L] - -def liftValuationSubring (f : K ≃+*v L) : 𝒪[K] ≃+*v 𝒪[L] := f.liftInteger - -instance liftValuationSubring.IsLocalRingHom {f : K ≃+*v L} : IsLocalRingHom (f.liftValuationSubring : 𝒪[K] →+* 𝒪[L]) := inferInstanceAs (_root_.IsLocalRingHom (ValRingHom.liftValuationSubring (f : K →+*v L))) - -def liftResidueField (f : K ≃+*v L) : 𝓀[K] ≃+* 𝓀[L] := LocalRing.ResidueField.mapEquiv (f.liftValuationSubring) -- TODO? : Should residue field be equipped with trivial valuation and enhance this to a ValRingHom? - -end ValRingEquiv - -namespace ValAlgebra - -variable {R A : Type*} [CommRing R] [Ring A] {ΓR ΓA: Type*} [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] [vR : Valued R ΓR] [vA : Valued A ΓA] [ValAlgebra R A] - --- `valuation_subring.algebra` instance as algebra Maria and Phillip gives instance on K₀ and L₀ L₀ := valuationSubring of extended valuation -instance liftInteger: ValAlgebra vR.v.integer vA.v.integer where - toValRingHom := ValAlgebra.toValRingHom.liftInteger - smul := fun ⟨r, _⟩ ⟨a, _⟩ => ⟨r • a, sorry⟩ - commutes' := fun ⟨r, _⟩ ⟨a, _⟩ => by ext; exact ValAlgebra.commutes' r a - smul_def' := fun ⟨r, _⟩ ⟨a, _⟩ => by ext; exact ValAlgebra.smul_def' r a - -variable {K L : Type*} [Field K] [Field L] {ΓK ΓL: Type*} [LinearOrderedCommGroupWithZero ΓK] [LinearOrderedCommGroupWithZero ΓL] [vK : Valued K ΓK] [vL : Valued L ΓL] [i : ValAlgebra K L] - -instance liftValuationSubring : ValAlgebra 𝒪[K] 𝒪[L] := inferInstanceAs (ValAlgebra vK.v.integer vL.v.integer) - -instance liftValuationSubring.IsLocalRingHom : IsLocalRingHom (algebraMap 𝒪[K] 𝒪[L]) := inferInstanceAs (_root_.IsLocalRingHom (i.toValRingHom).liftValuationSubring) - ---TODO : `Should add IsLocalAlgebra or LocalAlgebra to Mathlib` -instance liftResidueField : Algebra 𝓀[K] 𝓀[L] where - smul := sorry -- define this carefully, quotient from original action on 𝒪!! - toRingHom := LocalRing.ResidueField.map ((valAlgebraMap K L).liftValuationSubring) - commutes' := sorry - smul_def' := sorry -- TODO? : Should residue field be equipped with trivial valuation and enhance this to a ValRingHom? - -end ValAlgebra - -namespace ValAlgHom - -variable {R A B : Type*} [CommRing R] [Ring A] [Ring B] {ΓR ΓA ΓB : Type*} [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] [LinearOrderedCommGroupWithZero ΓB] [vR : Valued R ΓR] [vA : Valued A ΓA] [vB : Valued B ΓB] [ValAlgebra R A] [ValAlgebra R B] - -def liftInteger (s : A →ₐv[R] B) : vA.v.integer →ₐv[vR.v.integer] vB.v.integer where - toValRingHom := s.toValRingHom.liftInteger - commutes' _ := by ext; exact s.commutes' _ - -variable {K L L' : Type*} [Field K] [Field L] [Field L'] {ΓK ΓL ΓL': Type*} [LinearOrderedCommGroupWithZero ΓK] [LinearOrderedCommGroupWithZero ΓL] [LinearOrderedCommGroupWithZero ΓL'] [vK : Valued K ΓK] [vL : Valued L ΓL] [vL' : Valued L' ΓL'] [ValAlgebra K L] [ValAlgebra K L'] -- [FiniteDimensional K L] - -def liftValuationSubring (f : L →ₐv[K] L') : 𝒪[L] →ₐv[𝒪[K]] 𝒪[L'] := f.liftInteger - -instance liftValuationSubring.IsLocalRingHom {s : L →ₐv[K] L'}: IsLocalRingHom ((s.liftValuationSubring : 𝒪[L] →+*v 𝒪[L']) : 𝒪[L] →+* 𝒪[L']) := inferInstanceAs (_root_.IsLocalRingHom (s : L →+*v L').liftValuationSubring) - -def liftResidueField (f : L →ₐv[K] L') : 𝓀[L] →ₐ[𝓀[K]] 𝓀[L'] where - toRingHom := ValRingHom.liftResidueField f - commutes' := sorry -- by apply Quotient.ind - -end ValAlgHom - -namespace ValAlgEquiv - -variable {R A B : Type*} [CommRing R] [Ring A] [Ring B] {ΓR ΓA ΓB : Type*} [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] [LinearOrderedCommGroupWithZero ΓB] [vR : Valued R ΓR] [vA : Valued A ΓA] [vB : Valued B ΓB] [ValAlgebra R A] [ValAlgebra R B] - -def liftInteger (s : A ≃ₐv[R] B) : vA.v.integer ≃ₐv[vR.v.integer] vB.v.integer where - toValRingEquiv := s.toValRingEquiv.liftInteger - commutes' _ := by ext; exact s.commutes' _ - -variable {K L L' : Type*} [Field K] [Field L] [Field L'] {ΓK ΓL ΓL': Type*} [LinearOrderedCommGroupWithZero ΓK] [LinearOrderedCommGroupWithZero ΓL] [LinearOrderedCommGroupWithZero ΓL'] [vK : Valued K ΓK] [vL : Valued L ΓL] [vL' : Valued L' ΓL'] [ValAlgebra K L] [ValAlgebra K L'] -- [FiniteDimensional K L] - -def liftValuationSubring (f : L ≃ₐv[K] L') : 𝒪[L] ≃ₐv[𝒪[K]] 𝒪[L'] := f.liftInteger - -variable (s : L ≃ₐv[K] L') -#synth IsLocalRingHom (((s : L →ₐv[K] L') : L →+*v L').liftValuationSubring : 𝒪[L] →+* 𝒪[L']) --- #synth IsLocalRingHom (s.liftValuationSubring : 𝒪[L] →+* 𝒪[L']) -- this fails, this is the other way of a diamond, rfl to above but lean does not infer instances across rfl. -instance liftValuationSubring.IsLocalRingHom {s : L ≃ₐv[K] L'}: IsLocalRingHom ((s.liftValuationSubring : 𝒪[L] ≃+*v 𝒪[L']) : 𝒪[L] →+* 𝒪[L']) := inferInstanceAs (_root_.IsLocalRingHom ((s : L ≃+*v L') : L →+*v L').liftValuationSubring) - -def liftResidueField (f : L ≃ₐv[K] L') : 𝓀[L] ≃ₐ[𝓀[K]] 𝓀[L'] where - toEquiv := f.toValRingEquiv.liftResidueField - map_mul' := f.toValRingEquiv.liftResidueField.map_mul - map_add' := f.toValRingEquiv.liftResidueField.map_add - commutes' := sorry - --- should these be made into instances? `𝒪` and `𝓀` --- instance : Coe (ValAlgHom K L L') (ValAlgHom 𝒪[K] 𝒪[L] 𝒪[L']) := ⟨ValAlgHom.liftInteger⟩ - --- instance : Coe (ValAlgEquiv K L L') (ValAlgEquiv 𝒪[K] 𝒪[L] 𝒪[L']) := ⟨ValAlgEquiv.liftInteger⟩ - --- instance ... - -end ValAlgEquiv - -/- -def ValAlgHom.liftValuationIntegerQuotientleIdeal (s : L →ₐv[K] L) (γ : ΓL') : 𝒪[L]⧸(vL'.v.leIdeal γ) →ₐ[𝒪[K]] 𝒪[L']⧸(vL.leIdeal γ) := sorry - -def ValAlgIso.liftValuationIntegerQuotientleIdeal (s : L ≃ₐ[K] L) (γ : ΓL) : (𝒪[vL]⧸(vL.leIdeal γ)) ≃ₐ[𝒪[vK]] (𝒪[vL]⧸(vL.leIdeal γ)) := sorry - --- `LT version` - -def AlgHom.liftResidueField (s : L →ₐ[K] L) : 𝓀[vL] →ₐ[𝓀[vK]] 𝓀[vL] := sorry - -def AlgEquiv.liftResidueField (s : L ≃ₐ[K] L) : 𝓀[vL] ≃ₐ[𝓀[vK]] 𝓀[vL] := sorry - --/ - -namespace ValAlgEquiv - -section - -variable {K L L' : Type*} [CommRing K] [Ring L] [Ring L'] {ΓK ΓL ΓL': Type*} [LinearOrderedCommGroupWithZero ΓK] [LinearOrderedCommGroupWithZero ΓL] [LinearOrderedCommGroupWithZero ΓL'] [vK : Valued K ΓK] [vL : Valued L ΓL] [vL' : Valued L' ΓL'] [ValAlgebra K L] [ValAlgebra K L'] - -@[simp] -theorem coe_liftInteger {s : L ≃ₐv[K] L} {x : vL.v.integer} : ((s.liftInteger x) : L) = s x := rfl - -@[simp] -theorem liftInteger_refl : (.refl : L ≃ₐv[K] L).liftInteger = .refl := by - ext - rfl - -end - -section - -variable {K L L' : Type*} [CommRing K] [Field L] [Ring L'] {ΓK ΓL ΓL': Type*} [LinearOrderedCommGroupWithZero ΓK] [LinearOrderedCommGroupWithZero ΓL] [LinearOrderedCommGroupWithZero ΓL'] [vK : Valued K ΓK] [vL : Valued L ΓL] [vL' : Valued L' ΓL'] [ValAlgebra K L] [ValAlgebra K L'] - -@[simp] -theorem eq_refl_of_liftInteger_eq_refl {s : L ≃ₐv[K] L} : s.liftInteger = .refl ↔ s = .refl := by - constructor <;> - intro h - · ext l - obtain ⟨x, ⟨y, ⟨_, rfl⟩⟩⟩ := IsFractionRing.div_surjective l (A := 𝒪[L]) - calc - _ = ((s.liftInteger x) : L) / s.liftInteger y := by simp - _ = _ := by simp [h] - · simp [h] - -end - -end ValAlgEquiv diff --git a/RamificationGroup/Valuation/Discrete.lean b/RamificationGroup/Valuation/Discrete.lean index 195aec1..601daf6 100644 --- a/RamificationGroup/Valuation/Discrete.lean +++ b/RamificationGroup/Valuation/Discrete.lean @@ -5,7 +5,7 @@ import LocalClassFieldTheory.DiscreteValuationRing.Complete import LocalClassFieldTheory.DiscreteValuationRing.DiscreteNorm import RamificationGroup.ForMathlib.Henselian -import RamificationGroup.Valued.Defs +import Mathlib.Topology.Algebra.Valued.ValuedField import LocalClassFieldTheory.ForMathlib.RankOneValuation open Valuation Valued DiscreteValuation Multiplicative @@ -111,7 +111,7 @@ theorem pow_Uniformizer_all {x : K} (hx : x ≠ 0) (π : Uniformizer v) : rcases pow_Uniformizer v this π with ⟨n, u, hnu⟩ use n, u rw [show x = r.1 by rfl, hnu] - simp only [SubmonoidClass.coe_pow, zpow_coe_nat] + simp only [SubmonoidClass.coe_pow, zpow_natCast] · let r : v.valuationSubring := ⟨x⁻¹, h⟩ have : r ≠ 0 := by simp only [ne_eq, Subtype.ext_iff, ZeroMemClass.coe_zero, inv_eq_zero, hx, not_false_eq_true] rcases pow_Uniformizer v this π with ⟨n, u, hnu⟩ diff --git a/RamificationGroup/Valuation/Extension.lean b/RamificationGroup/Valuation/Extension.lean index b93e121..1d176ad 100644 --- a/RamificationGroup/Valuation/Extension.lean +++ b/RamificationGroup/Valuation/Extension.lean @@ -1,5 +1,3 @@ -/- --/ import Mathlib.RingTheory.DiscreteValuationRing.TFAE import Mathlib.FieldTheory.PrimitiveElement import RamificationGroup.ForMathlib.DiscreteValuationRing.Basic @@ -15,7 +13,7 @@ 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 [IsSeparable (ResidueField A) (ResidueField B)] +variable [Algebra.IsSeparable (ResidueField A) (ResidueField B)] variable [Module.Finite A B] instance : FiniteDimensional (ResidueField A) (ResidueField B) := FiniteDimensional_of_finite @@ -152,7 +150,7 @@ theorem irreducible_aeval_lift_redisue_primitive_add_irreducible_of_reducible_ae rw [hom_eval₂, algebraMap_residue_compat, ← eval₂_map, ← derivative_map] apply Separable.eval₂_derivative_ne_zero · rw [h_red] - apply IsSeparable.separable + apply Algebra.IsSeparable.isSeparable · rw [← aeval_def, h_red, minpoly.aeval] end x_and_f diff --git a/RamificationGroup/Valuation/PolyTaylor.lean b/RamificationGroup/Valuation/PolyTaylor.lean index 97a1a52..22a7bac 100644 --- a/RamificationGroup/Valuation/PolyTaylor.lean +++ b/RamificationGroup/Valuation/PolyTaylor.lean @@ -1,7 +1,3 @@ -/- -GOAL: -1. one order taylor expansion --/ import Mathlib.Algebra.Polynomial.Taylor namespace Polynomial diff --git a/RamificationGroup/Valuation/SubAlgEquiv.lean b/RamificationGroup/Valuation/SubAlgEquiv.lean index 0942840..39efe31 100644 --- a/RamificationGroup/Valuation/SubAlgEquiv.lean +++ b/RamificationGroup/Valuation/SubAlgEquiv.lean @@ -1,4 +1,4 @@ -import Mathlib.RingTheory.IntegrallyClosed +import Mathlib.RingTheory.Adjoin.Basic import Mathlib.Algebra.Polynomial.Induction section semiring diff --git a/RamificationGroup/Valued/Def'.lean b/RamificationGroup/Valued/Def'.lean new file mode 100644 index 0000000..e69de29 diff --git a/RamificationGroup/Valued/Defs.lean b/RamificationGroup/Valued/Defs.lean deleted file mode 100644 index ecd17f6..0000000 --- a/RamificationGroup/Valued/Defs.lean +++ /dev/null @@ -1,77 +0,0 @@ -import Mathlib.Topology.Algebra.Valuation - -namespace Valued - -/-- A `Valued` version of `Valuation.valuationSubring`, enabling the notation `𝒪[K]` for valued field `K` -/ -@[reducible] -def valuationSubring (K : Type*) [Field K] {Γ : outParam Type*} [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] : ValuationSubring K := (Valued.v).valuationSubring - -@[inherit_doc] -scoped notation "𝒪[" K "]" => Valued.valuationSubring K - -/-- An abbrevation for `LocalRing.maximalIdeal 𝒪[K]` of a valued field `K`, enabling the notation `𝓂[K]` -/ -@[reducible] -def maximalIdeal (K : Type*) [Field K] {Γ : outParam Type*} [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] : Ideal 𝒪[K] := LocalRing.maximalIdeal 𝒪[K] - -@[inherit_doc] -scoped notation "𝓂[" K "]" => maximalIdeal K - -/-- An abbrevation for `LocalRing.ResidueField 𝒪[K]` of a `Valued` instance, enabling the notation `𝓀[K]` -/ -@[reducible] -def ResidueField (K : Type*) [Field K] {Γ : outParam Type*} [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] := LocalRing.ResidueField (𝒪[K]) - -@[inherit_doc] -scoped notation:max "𝓀[" K:max "]" => ResidueField K - -end Valued - -/- - -section IntegerValued -variable (R K : Type*) [Ring R] [Field K] {Γ : outParam Type*} [LinearOrderedCommGroupWithZero Γ] [vR : Valued R Γ] [vK : Valued K Γ] - ---`Is this really needed now? when there is no need for ValHom` --- is this instance OK? or is it needed? If needed add simp lemmas saying `v (s.liftInteger x) = v (s x.val) ` -instance integer.valued: Valued vR.v.integer Γ := Valued.mk' (vR.v.comap vR.v.integer.subtype) - - --- need to add this, lean cannot infer this --- `This will be auto infered once Valuation.valuationSubring is with @[reducible] tag or at least @[instance]`, for now, every instance need to be written again for `𝒪[K]`, in this file and Hom.lift file and more. This is also the reason that valuationSubring should with tag @[reducible]. Add this tag to `Valuation.valuationSubring` when impoet to mathlib! -instance valuationSubring.valued: Valued 𝒪[K] Γ := inferInstanceAs (Valued vK.v.integer Γ) - -#synth Valued 𝒪[K] Γ -#synth LocalRing 𝒪[K] -#synth Algebra 𝒪[K] K - - -/- -- For `Valued.liftInteger` -theorem integer_valuation_eq : (Valued.integer.valued R).v = (vR.v.comap vR.v.integer.subtype) := rfl - -theorem integerAlgebraMap.monotone : Monotone (algebraMap 𝒪[K] K) := sorry - --- also value IsEquiv of O[K] and K -- they are equal! --- `First show val is equiv, then use theorem IsEquiv implies monotone and continuous!!!!!` --/ - -@[simp] -theorem integer_val_coe (x : vR.v.integer) : Valued.v x = Valued.v (x : R) := rfl - -@[simp] -theorem valuationSubring_val_coe (x : 𝒪[K]): v x = v (x : K) := rfl - -theorem integer_val_le_one (x : vR.v.integer) : Valued.v x ≤ 1 := (mem_integer_iff vR.v x.1).mp x.2 - -#check mem_integer_iff - -end IntegerValued - --/ - -/- -theorem maximalIdeal_eq {K : Type*} [Field K] {Γ : outParam Type*} [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] : 𝓂[K] = (Valued.v).ltIdeal 1 := sorry --/ - - - --- TODO? : Should residue field be equipped with trivial valuation? --- A generalization of this could be : after a valued ring quotient a "upper-closed" value ideal, it is equipped with a quotient valuation diff --git a/RamificationGroup/Valued/Hom/Discrete.lean b/RamificationGroup/Valued/Hom/Discrete.lean index c79059a..d353d27 100644 --- a/RamificationGroup/Valued/Hom/Discrete.lean +++ b/RamificationGroup/Valued/Hom/Discrete.lean @@ -66,7 +66,7 @@ theorem aeval_valuationSubring_lt_one_of_lt_one_self · simp only [coeff_map, h0, _root_.map_zero] theorem mem_integer_of_mem_integral_closure (h : vK.v.IsEquiv <| v.comap (algebraMap K L)) - {x : L} (hx : x ∈ integralClosure vK.valuationSubring L) : + {x : L} (hx : x ∈ integralClosure 𝒪[K] L) : x ∈ v.integer := by rcases hx with ⟨p, hp⟩ rw [mem_integer_iff] @@ -128,8 +128,9 @@ theorem extension_integer_eq_extendedValuation_of_discrete (h : vK.v.IsEquiv <| theorem integral_closure_eq_integer_of_complete_discrete (h : vK.v.IsEquiv <| vL.comap (algebraMap K L)) : - (integralClosure vK.valuationSubring L).toSubring = vL.integer := by - rw [Extension.integralClosure_eq_integer, extension_integer_eq_extendedValuation_of_discrete h] + (integralClosure 𝒪[K] L).toSubring = vL.integer := by + rw [show integralClosure 𝒪[K] L = integralClosure vK.v.valuationSubring L by rfl, + Extension.integralClosure_eq_integer, extension_integer_eq_extendedValuation_of_discrete h] ext rw [ValuationSubring.mem_toSubring, mem_valuationSubring_iff, mem_integer_iff] diff --git a/RamificationGroup/Valued/Hom/Lift.lean b/RamificationGroup/Valued/Hom/Lift.lean index 823cb26..e283ead 100644 --- a/RamificationGroup/Valued/Hom/Lift.lean +++ b/RamificationGroup/Valued/Hom/Lift.lean @@ -20,7 +20,7 @@ theorem ringHomClass_eq_iff_valuationSubring (f g : F) : · simp only [heq, Subtype.forall, mem_valuationSubring_iff, implies_true, forall_const] · apply DFunLike.ext intro x - rcases ValuationSubring.mem_or_inv_mem 𝒪[K] x with h | h + rcases ValuationSubring.mem_or_inv_mem vK.v.valuationSubring x with h | h · exact heq ⟨x, h⟩ · calc _ = (f x⁻¹)⁻¹ := by diff --git a/RamificationGroup/Valued/Hom/ValExtension.lean b/RamificationGroup/Valued/Hom/ValExtension.lean index 35fc35d..9b252bd 100644 --- a/RamificationGroup/Valued/Hom/ValExtension.lean +++ b/RamificationGroup/Valued/Hom/ValExtension.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Patrick Massot. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jiedong Jiang, Bichang Lei -/ -import RamificationGroup.Valued.Defs +import Mathlib.Topology.Algebra.Valued.ValuedField -- import Mathlib.Topology.Algebra.Valued.ValuedField /-! @@ -137,8 +137,7 @@ def ofValuationSubringComap {R A : Type*} {ΓR ΓA : outParam Type*} [Field R] [ [Algebra R A] [vR : Valued R ΓR] [vA : Valued A ΓA] [IsValExtension R A] (h : 𝒪[A].comap (algebraMap R A) = 𝒪[R]) : IsValExtension R A := by apply ofIntegerComap - rw [show vR.v.integer = 𝒪[R].toSubring by rfl, ← h] - rfl + rw [show vR.v.integer = 𝒪[R] by rfl, ← h] end mk' @@ -212,13 +211,14 @@ instance : Algebra 𝒪[R] 𝒪[A] := inferInstanceAs (Algebra vR.v.integer vA.v theorem coe_algebraMap_valuationSubring (r : 𝒪[R]) : ((algebraMap 𝒪[R] 𝒪[A]) r : A) = (algebraMap R A) (r : R) := rfl +#synth Algebra 𝒪[R] R instance : IsLocalRingHom (algebraMap 𝒪[R] 𝒪[A]) where map_nonunit r hr := by by_cases h : r = 0 · simp [h] at hr · apply Valuation.Integers.isUnit_of_one (v := vR.v) · exact Valuation.integer.integers (v := vR.v) - · simpa only [ValuationSubring.algebraMap_apply, isUnit_iff_ne_zero, ne_eq, + · simpa only [Algebra.algebraMap_ofSubring_apply, isUnit_iff_ne_zero, ne_eq, ZeroMemClass.coe_eq_zero] · apply Valuation.Integers.one_of_isUnit (Valuation.integer.integers (v := vA.v)) at hr change v (((algebraMap ↥𝒪[R] ↥𝒪[A]) r) : A) = 1 at hr diff --git a/lake-manifest.json b/lake-manifest.json index a7eb8b4..09360c3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,10 +1,11 @@ -{"version": 7, +{"version": "1.1.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "551ff2d7dffd7af914cdbd01abbd449fe3e3d428", + "scope": "leanprover-community", + "rev": "dc167d260ff7ee9849b436037add06bed15104be", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,7 +14,8 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6", + "scope": "leanprover-community", + "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,7 +24,8 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "53ba96ad7666d4a2515292974631629b5ea5dfee", + "scope": "leanprover-community", + "rev": "ae6ea60e9d8bc2d4b37ff02115854da2e1b710d0", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,25 +34,28 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5", + "scope": "leanprover-community", + "rev": "a96aee5245720f588876021b6a0aa73efee49c76", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.36", + "inputRev": "v0.0.41", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", + "scope": "", + "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/import-graph.git", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, - "rev": "77e081815b30b0d30707e1c5b0c6a6761f7a2404", + "scope": "leanprover-community", + "rev": "68cd8ae0f5b996176d1243d94c56e17de570e3bf", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,7 +64,8 @@ {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, - "rev": "322601e128d1dcfd5744436bed06471e126b417e", + "scope": "", + "rev": "604cb3610ee4c147dd3ef1966d0505c57cabbf0c", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -67,7 +74,8 @@ {"url": "https://github.com/PatrickMassot/checkdecls.git", "type": "git", "subDir": null, - "rev": "88ec21589a8eef430f4ea01147cde1aaa7963e16", + "scope": "", + "rev": "21a36f3c07a9229e1287483c16a0dd04e479ecc5", "name": "checkdecls", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -76,47 +84,12 @@ {"url": "https://github.com/mariainesdff/LocalClassFieldTheory.git", "type": "git", "subDir": null, - "rev": "9d4e28cb653faf63288501ba25baa78f28ef142c", + "scope": "", + "rev": "bf457847ed802fcf1e7c37026d22e68eb7b67fb9", "name": "local_class_field_theory", "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/xubaiw/CMark.lean", - "type": "git", - "subDir": null, - "rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05", - "name": "CMark", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "type": "git", - "subDir": null, - "rev": "effd8b8771cfd7ece69db99448168078e113c61f", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/hargonix/LeanInk", - "type": "git", - "subDir": null, - "rev": "f1f904e00d79a91ca6a76dec6e318531a7fd2a0f", - "name": "leanInk", - "manifestFile": "lake-manifest.json", - "inputRev": "doc-gen", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/doc-gen4", - "type": "git", - "subDir": null, - "rev": "c7f4ac84b973b6efd8f24ba2b006cad1b32c9c53", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "c7f4ac84b973b6efd8f24ba2b006cad1b32c9c53", - "inherited": false, "configFile": "lakefile.lean"}], "name": "RamificationGroup", "lakeDir": ".lake"} diff --git a/lean-toolchain b/lean-toolchain index ef1f67e..64981ae 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0 +leanprover/lean4:v4.11.0-rc1