Skip to content

Commit

Permalink
bump to nightly-2023-06-08-09
Browse files Browse the repository at this point in the history 
mathlib commit leanprover-community/mathlib@31c24aa
  • Loading branch information
@leanprover-community-bot
leanprover-community-bot committed Jun 8, 2023
1 parent 50cb46e commit a1bedf3
Show file tree
Hide file tree
Showing 3 changed files with 46 additions and 6 deletions.
40 changes: 40 additions & 0 deletions Mathbin/NumberTheory/RamificationInertia.lean
View file
Expand Up @@ -62,6 +62,7 @@ section DecEq

open scoped Classical

#print Ideal.ramificationIdx /-
/-- The ramification index of `P` over `p` is the largest exponent `n` such that
`p` is contained in `P^n`.
Expand All @@ -73,6 +74,7 @@ defined to be 0.
noncomputable def ramificationIdx : ℕ :=
sSup {n | map f p ≤ P ^ n}
#align ideal.ramification_idx Ideal.ramificationIdx
-/

variable {f p P}

Expand Down Expand Up @@ -186,6 +188,7 @@ variable (f p P)

attribute [local instance] Ideal.Quotient.field

#print Ideal.inertiaDeg /-
/-- The inertia degree of `P : ideal S` lying over `p : ideal R` is the degree of the
extension `(S / P) : (R / p)`.
Expand All @@ -203,7 +206,9 @@ noncomputable def inertiaDeg [hp : p.IsMaximal] : ℕ :=
Quotient.eq_zero_iff_mem.mpr <| mem_comap.mp <| hPp.symm ▸ ha
else 0
#align ideal.inertia_deg Ideal.inertiaDeg
-/

#print Ideal.inertiaDeg_of_subsingleton /-
-- Useful for the `nontriviality` tactic using `comap_eq_of_scalar_tower_quotient`.
@[simp]
theorem inertiaDeg_of_subsingleton [hp : p.IsMaximal] [hQ : Subsingleton (S ⧸ P)] :
Expand All @@ -213,7 +218,9 @@ theorem inertiaDeg_of_subsingleton [hp : p.IsMaximal] [hQ : Subsingleton (S ⧸
subst this
exact dif_neg fun h => hp.ne_top <| h.symm.trans comap_top
#align ideal.inertia_deg_of_subsingleton Ideal.inertiaDeg_of_subsingleton
-/

#print Ideal.inertiaDeg_algebraMap /-
@[simp]
theorem inertiaDeg_algebraMap [Algebra R S] [Algebra (R ⧸ p) (S ⧸ P)]
[IsScalarTower R (R ⧸ p) (S ⧸ P)] [hp : p.IsMaximal] :
Expand All @@ -228,6 +235,7 @@ theorem inertiaDeg_algebraMap [Algebra R S] [Algebra (R ⧸ p) (S ⧸ P)]
rw [Ideal.Quotient.lift_mk, ← Ideal.Quotient.algebraMap_eq, ← IsScalarTower.algebraMap_eq, ←
Ideal.Quotient.algebraMap_eq, ← IsScalarTower.algebraMap_apply]
#align ideal.inertia_deg_algebra_map Ideal.inertiaDeg_algebraMap
-/

end DecEq

Expand Down Expand Up @@ -486,11 +494,13 @@ section FactLeComap
-- mathport name: expre
local notation "e" => ramificationIdx f p P

#print Ideal.Quotient.algebraQuotientPowRamificationIdx /-
/-- `R / p` has a canonical map to `S / (P ^ e)`, where `e` is the ramification index
of `P` over `p`. -/
noncomputable instance Quotient.algebraQuotientPowRamificationIdx : Algebra (R ⧸ p) (S ⧸ P ^ e) :=
Quotient.algebraQuotientOfLeComap (Ideal.map_le_iff_le_comap.mp le_pow_ramificationIdx)
#align ideal.quotient.algebra_quotient_pow_ramification_idx Ideal.Quotient.algebraQuotientPowRamificationIdx
-/

@[simp]
theorem Quotient.algebraMap_quotient_pow_ramificationIdx (x : R) :
Expand All @@ -502,13 +512,15 @@ variable [hfp : NeZero (ramificationIdx f p P)]

include hfp

#print Ideal.Quotient.algebraQuotientOfRamificationIdxNeZero /-
/-- If `P` lies over `p`, then `R / p` has a canonical map to `S / P`.
This can't be an instance since the map `f : R → S` is generally not inferrable.
-/
def Quotient.algebraQuotientOfRamificationIdxNeZero : Algebra (R ⧸ p) (S ⧸ P) :=
Quotient.algebraQuotientOfLeComap (le_comap_of_ramificationIdx_ne_zero hfp.out)
#align ideal.quotient.algebra_quotient_of_ramification_idx_ne_zero Ideal.Quotient.algebraQuotientOfRamificationIdxNeZero
-/

-- In this file, the value for `f` can be inferred.
attribute [local instance] Ideal.Quotient.algebraQuotientOfRamificationIdxNeZero
Expand Down Expand Up @@ -540,6 +552,7 @@ theorem powQuotSuccInclusion_injective (i : ℕ) :
rwa [pow_quot_succ_inclusion_apply_coe] at hx0
#align ideal.pow_quot_succ_inclusion_injective Ideal.powQuotSuccInclusion_injective

#print Ideal.quotientToQuotientRangePowQuotSuccAux /-
/-- `S ⧸ P` embeds into the quotient by `P^(i+1) ⧸ P^e` as a subspace of `P^i ⧸ P^e`.
See `quotient_to_quotient_range_pow_quot_succ` for this as a linear map,
and `quotient_range_pow_quot_succ_inclusion_equiv` for this as a linear equivalence.
Expand All @@ -555,15 +568,19 @@ noncomputable def quotientToQuotientRangePowQuotSuccAux {i : ℕ} {a : S} (a_mem
rw [pow_quot_succ_inclusion_apply_coe, Subtype.coe_mk, Submodule.coe_sub, Subtype.coe_mk,
Subtype.coe_mk, _root_.map_mul, map_sub, sub_mul]
#align ideal.quotient_to_quotient_range_pow_quot_succ_aux Ideal.quotientToQuotientRangePowQuotSuccAux
-/

#print Ideal.quotientToQuotientRangePowQuotSuccAux_mk /-
theorem quotientToQuotientRangePowQuotSuccAux_mk {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) (x : S) :
quotientToQuotientRangePowQuotSuccAux f p P a_mem (Submodule.Quotient.mk x) =
Submodule.Quotient.mk ⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_left _ x a_mem)⟩ :=
by apply Quotient.map'_mk''
#align ideal.quotient_to_quotient_range_pow_quot_succ_aux_mk Ideal.quotientToQuotientRangePowQuotSuccAux_mk
-/

include hfp

#print Ideal.quotientToQuotientRangePowQuotSucc /-
/-- `S ⧸ P` embeds into the quotient by `P^(i+1) ⧸ P^e` as a subspace of `P^i ⧸ P^e`. -/
noncomputable def quotientToQuotientRangePowQuotSucc {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) :
S ⧸ P →ₗ[R ⧸ p] (P ^ i).map (P ^ e).Quotient.mk ⧸ (powQuotSuccInclusion f p P i).range
Expand All @@ -586,13 +603,17 @@ noncomputable def quotientToQuotientRangePowQuotSucc {i : ℕ} {a : S} (a_mem :
Ideal.Quotient.mk_eq_mk, Submodule.coe_smul_of_tower,
Ideal.Quotient.algebraMap_quotient_pow_ramificationIdx]
#align ideal.quotient_to_quotient_range_pow_quot_succ Ideal.quotientToQuotientRangePowQuotSucc
-/

#print Ideal.quotientToQuotientRangePowQuotSucc_mk /-
theorem quotientToQuotientRangePowQuotSucc_mk {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) (x : S) :
quotientToQuotientRangePowQuotSucc f p P a_mem (Submodule.Quotient.mk x) =
Submodule.Quotient.mk ⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_left _ x a_mem)⟩ :=
quotientToQuotientRangePowQuotSuccAux_mk f p P a_mem x
#align ideal.quotient_to_quotient_range_pow_quot_succ_mk Ideal.quotientToQuotientRangePowQuotSucc_mk
-/

#print Ideal.quotientToQuotientRangePowQuotSucc_injective /-
theorem quotientToQuotientRangePowQuotSucc_injective [IsDomain S] [IsDedekindDomain S] [P.IsPrime]
{i : ℕ} (hi : i < e) {a : S} (a_mem : a ∈ P ^ i) (a_not_mem : a ∉ P ^ (i + 1)) :
Function.Injective (quotientToQuotientRangePowQuotSucc f p P a_mem) := fun x =>
Expand All @@ -613,6 +634,7 @@ theorem quotientToQuotientRangePowQuotSucc_injective [IsDomain S] [IsDedekindDom
((Submodule.sub_mem_iff_right _ hz).mp (Pe_le_Pi1 h))).resolve_right
a_not_mem
#align ideal.quotient_to_quotient_range_pow_quot_succ_injective Ideal.quotientToQuotientRangePowQuotSucc_injective
-/

theorem quotientToQuotientRangePowQuotSucc_surjective [IsDomain S] [IsDedekindDomain S]
(hP0 : P ≠ ⊥) [hP : P.IsPrime] {i : ℕ} (hi : i < e) {a : S} (a_mem : a ∈ P ^ i)
Expand Down Expand Up @@ -741,35 +763,46 @@ open scoped Classical

variable [IsDomain S] [IsDedekindDomain S] [Algebra R S]

#print Ideal.Factors.ne_bot /-
theorem Factors.ne_bot (P : (factors (map (algebraMap R S) p)).toFinset) : (P : Ideal S) ≠ ⊥ :=
(prime_of_factor _ (Multiset.mem_toFinset.mp P.2)).NeZero
#align ideal.factors.ne_bot Ideal.Factors.ne_bot
-/

#print Ideal.Factors.isPrime /-
instance Factors.isPrime (P : (factors (map (algebraMap R S) p)).toFinset) :
IsPrime (P : Ideal S) :=
Ideal.isPrime_of_prime (prime_of_factor _ (Multiset.mem_toFinset.mp P.2))
#align ideal.factors.is_prime Ideal.Factors.isPrime
-/

#print Ideal.Factors.ramificationIdx_ne_zero /-
theorem Factors.ramificationIdx_ne_zero (P : (factors (map (algebraMap R S) p)).toFinset) :
ramificationIdx (algebraMap R S) p P ≠ 0 :=
IsDedekindDomain.ramificationIdx_ne_zero (ne_zero_of_mem_factors (Multiset.mem_toFinset.mp P.2))
(Factors.isPrime p P) (Ideal.le_of_dvd (dvd_of_mem_factors (Multiset.mem_toFinset.mp P.2)))
#align ideal.factors.ramification_idx_ne_zero Ideal.Factors.ramificationIdx_ne_zero
-/

#print Ideal.Factors.fact_ramificationIdx_neZero /-
instance Factors.fact_ramificationIdx_neZero (P : (factors (map (algebraMap R S) p)).toFinset) :
NeZero (ramificationIdx (algebraMap R S) p P) :=
⟨Factors.ramificationIdx_ne_zero p P⟩
#align ideal.factors.fact_ramification_idx_ne_zero Ideal.Factors.fact_ramificationIdx_neZero
-/

attribute [local instance] quotient.algebra_quotient_of_ramification_idx_ne_zero

#print Ideal.Factors.isScalarTower /-
instance Factors.isScalarTower (P : (factors (map (algebraMap R S) p)).toFinset) :
IsScalarTower R (R ⧸ p) (S ⧸ (P : Ideal S)) :=
IsScalarTower.of_algebraMap_eq fun x => by simp
#align ideal.factors.is_scalar_tower Ideal.Factors.isScalarTower
-/

attribute [local instance] Ideal.Quotient.field

#print Ideal.Factors.finrank_pow_ramificationIdx /-
theorem Factors.finrank_pow_ramificationIdx [p.IsMaximal]
(P : (factors (map (algebraMap R S) p)).toFinset) :
finrank (R ⧸ p) (S ⧸ (P : Ideal S) ^ ramificationIdx (algebraMap R S) p P) =
Expand All @@ -778,7 +811,9 @@ theorem Factors.finrank_pow_ramificationIdx [p.IsMaximal]
rw [finrank_prime_pow_ramification_idx, inertia_deg_algebra_map]
exact factors.ne_bot p P
#align ideal.factors.finrank_pow_ramification_idx Ideal.Factors.finrank_pow_ramificationIdx
-/

#print Ideal.Factors.finiteDimensional_quotient /-
instance Factors.finiteDimensional_quotient [IsNoetherian R S] [p.IsMaximal]
(P : (factors (map (algebraMap R S) p)).toFinset) :
FiniteDimensional (R ⧸ p) (S ⧸ (P : Ideal S)) :=
Expand All @@ -787,12 +822,16 @@ instance Factors.finiteDimensional_quotient [IsNoetherian R S] [p.IsMaximal]
isNoetherian_of_surjective S (Ideal.Quotient.mkₐ _ _).toLinearMap <|
LinearMap.range_eq_top.mpr Ideal.Quotient.mk_surjective
#align ideal.factors.finite_dimensional_quotient Ideal.Factors.finiteDimensional_quotient
-/

#print Ideal.Factors.inertiaDeg_ne_zero /-
theorem Factors.inertiaDeg_ne_zero [IsNoetherian R S] [p.IsMaximal]
(P : (factors (map (algebraMap R S) p)).toFinset) : inertiaDeg (algebraMap R S) p P ≠ 0 := by
rw [inertia_deg_algebra_map]; exact (finite_dimensional.finrank_pos_iff.mpr inferInstance).ne'
#align ideal.factors.inertia_deg_ne_zero Ideal.Factors.inertiaDeg_ne_zero
-/

#print Ideal.Factors.finiteDimensional_quotient_pow /-
instance Factors.finiteDimensional_quotient_pow [IsNoetherian R S] [p.IsMaximal]
(P : (factors (map (algebraMap R S) p)).toFinset) :
FiniteDimensional (R ⧸ p) (S ⧸ (P : Ideal S) ^ ramificationIdx (algebraMap R S) p P) :=
Expand All @@ -801,6 +840,7 @@ instance Factors.finiteDimensional_quotient_pow [IsNoetherian R S] [p.IsMaximal]
rw [pos_iff_ne_zero, factors.finrank_pow_ramification_idx]
exact mul_ne_zero (factors.ramification_idx_ne_zero p P) (factors.inertia_deg_ne_zero p P)
#align ideal.factors.finite_dimensional_quotient_pow Ideal.Factors.finiteDimensional_quotient_pow
-/

universe w

Expand Down
8 changes: 4 additions & 4 deletions lake-manifest.json
View file
Expand Up @@ -10,15 +10,15 @@
{"git":
{"url": "https://github.com/leanprover-community/lean3port.git",
"subDir?": null,
"rev": "c97a97706688b46f41ff2cb05cbd8bef71b3068f",
"rev": "4a6eaf0fa8f530048dde8b60e336409aa5ae6cb9",
"name": "lean3port",
"inputRev?": "c97a97706688b46f41ff2cb05cbd8bef71b3068f"}},
"inputRev?": "4a6eaf0fa8f530048dde8b60e336409aa5ae6cb9"}},
{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
"rev": "622179856b2c216c6827cf951693ead10362691f",
"rev": "9dff81adeb78d78b58d8302a67b9b7fce1a96709",
"name": "mathlib",
"inputRev?": "622179856b2c216c6827cf951693ead10362691f"}},
"inputRev?": "9dff81adeb78d78b58d8302a67b9b7fce1a96709"}},
{"git":
{"url": "https://github.com/gebner/quote4",
"subDir?": null,
Expand Down
4 changes: 2 additions & 2 deletions lakefile.lean
View file
Expand Up @@ -4,7 +4,7 @@ open Lake DSL System
-- Usually the `tag` will be of the form `nightly-2021-11-22`.
-- If you would like to use an artifact from a PR build,
-- it will be of the form `pr-branchname-sha`.
def tag : String := "nightly-2023-06-08-07"
def tag : String := "nightly-2023-06-08-09"
def releaseRepo : String := "leanprover-community/mathport"
def oleanTarName : String := "mathlib3-binport.tar.gz"

Expand Down Expand Up @@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
untarReleaseArtifact releaseRepo tag oleanTarName libDir
return .nil

require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"c97a97706688b46f41ff2cb05cbd8bef71b3068f"
require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"4a6eaf0fa8f530048dde8b60e336409aa5ae6cb9"

@[default_target]
lean_lib Mathbin where
Expand Down

0 comments on commit a1bedf3

Please sign in to comment.