Algebraic Hartogs principle for… to Krull–Akizuki for Mathlib's…
TheoremAlgebraic Hartogs principle for fractions#
Let R be a Noetherian local ring of depth at
least two with total ring of fractions K. An element of K that lies in the image of R_p for
every prime p other than the maximal ideal lies in R: if for every such p some t ∉ p has
t x ∈ R, then x ∈ R.
IsLocalRing.mem_range_algebraMap_of_two_le_depth.{u, u_1} {R : Type u} [CommRing R] [IsLocalRing R]
[IsNoetherianRing R] (K : Type u_1) [CommRing K] [Algebra R K] [IsFractionRing R K]
(hdepth : 2 ≤ IsLocalRing.depth ↧R) {x : K}
(hx :
∀ (p : Ideal R) [p.IsPrime],
p ≠ IsLocalRing.maximalIdeal R → ∃ t ∉ p, (algebraMap R K) t * x ∈ (algebraMap R K).range) :
x ∈ (algebraMap R K).range
Lean
Formalized in Tau Ceti as IsLocalRing.mem_range_algebraMap_of_two_le_depth.
Sources
TheoremThe Auslander–Buchsbaum formula#
For a nonzero finite module M of finite projective
dimension over a Noetherian local ring R, projectiveDimension M + depth M = depth R.
Stacks, Proposition 10.111.1 (090V).
ModuleCat.projectiveDimension_add_depth_eq_depth.{v, u} {R : Type u} [CommRing R] [IsLocalRing R]
[IsNoetherianRing R] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] [Nontrivial ↑M]
(hM : CategoryTheory.projectiveDimension M ≠ ⊤) :
CategoryTheory.projectiveDimension M + ↑(IsLocalRing.depth M) = ↑(IsLocalRing.depth ↧R)
TheoremThe Cauchy estimate at unit radius#
Hasse derivatives do not increase the Gauss norm of an overconvergent series.
TauCeti.Dagger.washnitzerAlgebra.norm_toTate_hasseDeriv_le.{u_1, u_2} {σ : Type u_1} {R : Type u_2}
[NormedCommRing R] [IsUltrametricDist R] (d : σ →₀ ℕ)
(f : ↥(TauCeti.Dagger.washnitzerAlgebra σ R)) :
‖(TauCeti.Dagger.washnitzerAlgebra.toTate σ R)
((TauCeti.Dagger.washnitzerAlgebra.hasseDeriv σ R d) f)‖ ≤
‖(TauCeti.Dagger.washnitzerAlgebra.toTate σ R) f‖
Lean
Formalized in Tau Ceti as TauCeti.Dagger.washnitzerAlgebra.norm_toTate_hasseDeriv_le.
Sources
Uses 3
TheoremChase–Harrison–Rosenberg (TauCeti.Algebra.isFiniteEtaleTorsor_iff)#
B is a finite étale G-torsor over A if and only if
A → B is injective, A is the ring of invariants, and the action is free: for each g ≠ 1 the
elements g • b - b generate the unit ideal of B.
TauCeti.Algebra.isFiniteEtaleTorsor_iff.{u_1, u_2, u_3} {G : Type u_1} {A : Type u_2} {B : Type u_3}
[Group G] [CommRing A] [CommRing B] [Algebra A B] [MulSemiringAction G B] [SMulCommClass G A B]
[Finite G] :
TauCeti.Algebra.IsFiniteEtaleTorsor G A B ↔
FaithfulSMul A B ∧
Algebra.IsInvariant A B G ∧ ∀ (g : G), g ≠ 1 → Ideal.span (Set.range fun b => g • b - b) = ⊤
TheoremChase–Harrison–Rosenberg (TauCeti.MulSemiringAction.tensorToPi_bijective)#
For a free action of a finite group with invariant ring R,
tensorToPi : A ⊗[R] A → (G → A) is bijective.
TauCeti.MulSemiringAction.tensorToPi_bijective.{u_1, u_2, u_3} {R : Type u_1} {A : Type u_2}
{G : Type u_3} [CommSemiring R] [CommRing A] [Algebra R A] [Group G] [MulSemiringAction G A]
[SMulCommClass G R A] [Algebra.IsInvariant R A G] [Finite G]
(hG : ∀ (g : G), g ≠ 1 → Ideal.span (Set.range fun a => g • a - a) = ⊤) :
Function.Bijective ⇑(TauCeti.MulSemiringAction.tensorToPi R A G)
Lean
Formalized in Tau Ceti as TauCeti.MulSemiringAction.tensorToPi_bijective.
Other forms
Chase–Harrison–Rosenberg. Formalized in Tau Ceti as TauCeti.MulSemiringAction.tensorToPi_surjective_iff.
TauCeti.MulSemiringAction.tensorToPi_surjective_iff.{u_1, u_2, u_3} {R : Type u_1} {A : Type u_2}
{G : Type u_3} [CommSemiring R] [CommRing A] [Algebra R A] [Group G] [MulSemiringAction G A]
[SMulCommClass G R A] [Finite G] :
Function.Surjective ⇑(TauCeti.MulSemiringAction.tensorToPi R A G) ↔
∀ (g : G), g ≠ 1 → Ideal.span (Set.range fun a => g • a - a) = ⊤
Sources
Used by 1
DefinitionChinese Remainder Theorem for AdjoinRoot#
for f nonzero and squarefree,
K[X] ⧸ (f) is the product of the fields K[X] ⧸ (p) over the monic irreducible factors p
of f.
AdjoinRoot.equivPiFactors.{u_1} {K : Type u_1} [Field K] {f : Polynomial K} (hf : f ≠ 0)
(hsq : Squarefree f) : AdjoinRoot f ≃ₐ[K] (p : f.Factors) → AdjoinRoot ↑p
Used by 2
TheoremCramer's bound for subalgebras of integral elements#
Let e be an F-basis of E lying in
an R-subalgebra Γ all of whose elements are integral over the integrally closed domain R, and
let r = det (Tr_F (e i * e j)) be the Gram determinant of the regular trace form. Then r • x
lies in the R-span of e for every x ∈ Γ.
TauCeti.IntegralOrder.det_smul_mem_span.{u_1, u_2, u_3, u_4} {R : Type u_1} {F : Type u_2}
{E : Type u_3} [CommRing R] [Field F] [Ring E] [Algebra R F] [IsFractionRing R F] [Algebra F E]
[Algebra R E] [IsScalarTower R F E] [FiniteDimensional F E] [IsIntegrallyClosed R] {ι : Type u_4}
[Fintype ι] [DecidableEq ι] (e : Module.Basis ι F E) {Γ : Subalgebra R E}
(he : ∀ (i : ι), e i ∈ Γ) (hint : ∀ x ∈ Γ, IsIntegral R x) {x : E} (hx : x ∈ Γ) :
((LinearMap.BilinForm.toMatrix e) (Algebra.regularTraceForm F E)).det • x ∈
Submodule.span R (Set.range ⇑e)
TheoremDedekind's different theorem, the tame case, as an exponent#
the multiplicity of P in
the different ideal is exactly e(P ∣ p) - 1 when the residue extension is separable and
e(P ∣ p) is nonzero in the residue field A ⧸ p.
TauCeti.multiplicity_differentIdeal_eq_ramificationIdx_sub_one_iff.{u_1, u_2} (A : Type u_1)
{B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B]
[Module.IsTorsionFree A B] [Module.Finite A B]
[Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] (hp : p ≠ ⊥)
(P : Ideal B) [P.IsMaximal] [P.LiesOver p] :
multiplicity P (differentIdeal A B) = P.ramificationIdx A - 1 ↔
Algebra.IsSeparable (A ⧸ p) (B ⧸ P) ∧ ↑(P.ramificationIdx A) ≠ 0
Lean
Formalized in Tau Ceti as TauCeti.multiplicity_differentIdeal_eq_ramificationIdx_sub_one_iff.
Other forms
Dedekind's different theorem at a prime power with a coprime complement. Formalized in Tau Ceti as TauCeti.pow_dvd_differentIdeal_iff_of_isCoprime.
TauCeti.pow_dvd_differentIdeal_iff_of_isCoprime.{u_1, u_2} (A : Type u_1) {B : Type u_2}
[CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B]
[Module.IsTorsionFree A B] [Module.Finite A B]
[Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] (hp : p ≠ ⊥)
(P Q : Ideal B) [P.IsMaximal] [P.LiesOver p] {e : ℕ} (hPQ : IsCoprime (P ^ e) Q)
(hmul : P ^ e * Q = Ideal.map (algebraMap A B) p) :
P ^ e ∣ differentIdeal A B ↔ ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P) ∨ ↑e = 0
Dedekind's different theorem, first part, as a bound on the exponent. Formalized in Tau Ceti as TauCeti.ramificationIdx_sub_one_le_multiplicity_differentIdeal.
TauCeti.ramificationIdx_sub_one_le_multiplicity_differentIdeal.{u_1, u_2} (A : Type u_1)
{B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B]
[Module.IsTorsionFree A B] [Module.Finite A B]
[Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] (hp : p ≠ ⊥)
(P : Ideal B) [P.IsPrime] [P.LiesOver p] :
P.ramificationIdx A - 1 ≤ multiplicity P (differentIdeal A B)
Dedekind's different theorem, second part (Stichtenoth, Theorem 3.5.1(b) and Corollary 3.5.5). Formalized in Tau Ceti as TauCeti.pow_ramificationIdx_dvd_differentIdeal_iff.
TauCeti.pow_ramificationIdx_dvd_differentIdeal_iff.{u_1, u_2} (A : Type u_1) {B : Type u_2}
[CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B]
[Module.IsTorsionFree A B] [Module.Finite A B]
[Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] (hp : p ≠ ⊥)
(P : Ideal B) [P.IsMaximal] [P.LiesOver p] :
P ^ P.ramificationIdx A ∣ differentIdeal A B ↔
¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P) ∨ ↑(P.ramificationIdx A) = 0
Dedekind's different theorem, second part, as a bound on the exponent. Formalized in Tau Ceti as TauCeti.ramificationIdx_le_multiplicity_differentIdeal_iff.
TauCeti.ramificationIdx_le_multiplicity_differentIdeal_iff.{u_1, u_2} (A : Type u_1) {B : Type u_2}
[CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B]
[Module.IsTorsionFree A B] [Module.Finite A B]
[Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] (hp : p ≠ ⊥)
(P : Ideal B) [P.IsMaximal] [P.LiesOver p] :
P.ramificationIdx A ≤ multiplicity P (differentIdeal A B) ↔
¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P) ∨ ↑(P.ramificationIdx A) = 0
Sources
TheoremEuler's criterion in a finite residue domain#
Let P be a prime of R with finite
quotient and n ∣ #(R ⧸ P) - 1. For a ∉ P, the class of a is an n-th power in R ⧸ P
exactly when a ^ ((#(R ⧸ P) - 1) / n) ≡ 1 (mod P).
Ideal.exists_pow_eq_mk_iff_pow_sub_one_mem.{u_1} {R : Type u_1} [CommRing R] {P : Ideal R}
[P.IsPrime] [Finite (R ⧸ P)] {n : ℕ} (hdvd : n ∣ Nat.card (R ⧸ P) - 1) {a : R} (ha : a ∉ P) :
(∃ b, b ^ n = (Ideal.Quotient.mk P) a) ↔ a ^ ((Nat.card (R ⧸ P) - 1) / n) - 1 ∈ P
Uses 1 · Used by 1
TheoremThe Frobenius surjectivity criterion#
The Frobenius surjectivity criterion (Bhatt–Morrow–Scholze, Integral p-adic Hodge
theory, Lemma 3.9). In a π-adically complete and separated ring A with π ^ p ∣ p, the
following are equivalent: every element of A is a p-th power modulo π ^ p, modulo p, and
modulo π p.
TauCeti.tfae_forall_exists_dvd_sub_pow.{u_1} {A : Type u_1} [CommRing A] (π : A) {p : ℕ}
[Fact (Nat.Prime p)] [IsHausdorff (Ideal.span {π}) A] [IsPrecomplete (Ideal.span {π}) A]
(h : π ^ p ∣ ↑p) :
[∀ (x : A), ∃ y, π ^ p ∣ x - y ^ p, ∀ (x : A), ∃ y, ↑p ∣ x - y ^ p,
∀ (x : A), ∃ y, π * ↑p ∣ x - y ^ p].TFAE
TheoremThe graded Nakayama lemma for generators#
If a set s of homogeneous elements of positive
degree generates the irrelevant ideal A₊ of an ℕ-graded commutative semiring modulo A₊², then
s generates the semiring as an algebra over its degree-zero part.
TauCeti.GradedAlgebra.adjoin_eq_top_of_irrelevant_le.{u_1, u_2} {A : Type u_1} {σ : Type u_2}
[CommSemiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {s : Set A}
(hs : ∀ x ∈ s, ∃ i, 0 < i ∧ x ∈ 𝒜 i)
(h :
(HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤
Ideal.span s ⊔ (HomogeneousIdeal.irrelevant 𝒜).toIdeal ^ 2) :
Algebra.adjoin (↥(𝒜 0)) s = ⊤
Lean
Formalized in Tau Ceti as TauCeti.GradedAlgebra.adjoin_eq_top_of_irrelevant_le.
Sources
TheoremThe Hadamard three circles inequality on 𝕎 O[1/(p [ϖ])]#
For radii
ρ₁ ≤ ρ ≤ ρ₂, the Gauss valuation λ_ρ is bounded by the larger of λ_{ρ₁} and λ_{ρ₂}, so
the interval norm of an interval dominates every Gauss valuation at a radius inside it.
TauCeti.WittVector.gaussValuationAway_le_max.{u_1, u_2, u_3} {p : ℕ} [Fact (Nat.Prime p)]
{K : Type u_1} {O : Type u_2} [Field K] [CommRing O] [Algebra O K] {v : Valuation K NNReal}
{ϖ : O} [CharP O p] [PerfectRing O p] {B : Type u_3} [CommRing B] [Algebra (WittVector p O) B]
[IsLocalization.Away (↑p * (WittVector.teichmuller p) ϖ) B] (hv : v.Integers O) (hϖ : ϖ ≠ 0)
{ρ ρ₁ ρ₂ : NNReal} (hρ : ρ ∈ Set.Ioo 0 1) (hρ₁ : ρ₁ ∈ Set.Ioo 0 1) (hρ₂ : ρ₂ ∈ Set.Ioo 0 1)
(h₁ : ρ₁ ≤ ρ) (h₂ : ρ ≤ ρ₂) (x : B) :
(TauCeti.WittVector.gaussValuationAway p hv hϖ ρ hρ B) x ≤
max ((TauCeti.WittVector.gaussValuationAway p hv hϖ ρ₁ hρ₁ B) x)
((TauCeti.WittVector.gaussValuationAway p hv hϖ ρ₂ hρ₂ B) x)
Lean
Formalized in Tau Ceti as TauCeti.WittVector.gaussValuationAway_le_max.
Other forms
The Hadamard three circles inequality for Gauss valuations. Formalized in Tau Ceti as TauCeti.WittVector.gaussValuation_mul_inv_pow_le_max.
TauCeti.WittVector.gaussValuation_mul_inv_pow_le_max.{u_1, u_2} {p : ℕ} [Fact (Nat.Prime p)]
{K : Type u_1} {O : Type u_2} [Field K] [CommRing O] [Algebra O K] [CharP O p] [PerfectRing O p]
{v : Valuation K NNReal} {ρ : NNReal} (hv : v.Integers O) {ρ₁ ρ₂ : NNReal} (hρ : ρ < 1)
(hρ₁ : ρ₁ < 1) (hρ₂ : ρ₂ < 1) (h₀ : 0 < ρ₁) (h₁ : ρ₁ ≤ ρ) (h₂ : ρ ≤ ρ₂) (x : WittVector p O)
(m : ℕ) :
(TauCeti.WittVector.gaussValuation p hv ρ hρ) x * (ρ ^ m)⁻¹ ≤
max ((TauCeti.WittVector.gaussValuation p hv ρ₁ hρ₁) x * (ρ₁ ^ m)⁻¹)
((TauCeti.WittVector.gaussValuation p hv ρ₂ hρ₂) x * (ρ₂ ^ m)⁻¹)
Sources
TheoremHazewinkel's functional equation lemma#
Let f = b₁ X + ⋯ be a formal coordinate over K
whose linear coefficient b₁ is a unit of A, and suppose that f satisfies the functional
equation. Then the formal group law f⁻¹(f(X) + f(Y)) with logarithm f, the transport
f⁻¹ • 𝔾ₐ of the additive formal group law, has all its coefficients in A.
TauCeti.coeff_inv_smul_𝔾ₐ_toPowerSeries_mem.{u_1} {K : Type u_1} [CommRing K] {p : ℕ}
[hp : Fact (Nat.Prime p)] {σ : K →+* K} {s : ℕ → K} {A : Subring K} (hσ : Set.MapsTo ⇑σ ↑A ↑A)
(hσp : ∀ a ∈ A, ∃ b ∈ A, σ a - a ^ p = ↑p * b) (hs : ∀ (i : ℕ), ↑p * s i ∈ A)
(f : TauCeti.FormalCoordinate K) (hf₁ : ∃ u ∈ A, u * (PowerSeries.coeff 1) f.toPowerSeries = 1)
(hf : TauCeti.SatisfiesFunctionalEquation p σ s A f.toPowerSeries) (d : Fin 2 →₀ ℕ) :
(MvPowerSeries.coeff d) (f⁻¹ • FormalGroup.𝔾ₐ).toPowerSeries ∈ A
Uses 1
TheoremHensel's lemma for the norm#
Let S be a finite free algebra over a ring R Henselian at
an ideal I, containing a unit w whose trace is a unit. If a unit v of R is congruent to the
norm of a modulo I, then v is the norm of some y congruent to a modulo IS.
TauCeti.Algebra.exists_norm_eq_of_norm_sub_mem.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R]
[CommRing S] [Algebra R S] [Module.Free R S] [Module.Finite R S] {I : Ideal R} [HenselianRing R I]
{w : S} (hw : IsUnit w) (htr : IsUnit ((Algebra.trace R S) w)) {a : S} {v : R} (hv : IsUnit v)
(hav : (Algebra.norm R) a - v ∈ I) :
∃ y, (Algebra.norm R) y = v ∧ y - a ∈ Ideal.map (algebraMap R S) I
Used by 26
ℚ_p · A Kummer cup over a local field is its Hilbert symbol times a fixed nonzero cup · Hilbert's product formula · Local classification (O'Meara 63:20, Serre IV Thm 7) · The relative Stiefel–Whitney formula over a local field · Tate's duality on an open subgroup acting trivially on μₙ · The cyclic Hasse norm theorem · The Hasse principle for Brauer classes, from idele-class H¹ · The Kronecker–Weber theorem · The Kummer case of the second fundamental inequality · Hasse--Arf in prime degree · The finite level of the generator theorem (NSW, proof of (7.4.1))
TheoremHensel's lemma with a derivative dividing π ^ k#
Let R be π-adically complete with
π a non-zero-divisor, and let f be a polynomial with f'(t) ∣ π ^ k and
f(t) ≡ 0 mod π ^ (2k + 1). Then f has exactly one root congruent to t modulo π ^ (k + 1).
TauCeti.IsAdicComplete.existsUnique_eval_eq_zero_of_dvd_pow.{u_1} {R : Type u_1} [CommRing R]
{π : R} {f : Polynomial R} {k : ℕ} {t : R} [IsAdicComplete (Ideal.span {π}) R]
(hπ : IsLeftRegular π) (hd : Polynomial.eval t (Polynomial.derivative f) ∣ π ^ k)
(ht : π ^ (2 * k + 1) ∣ Polynomial.eval t f) : ∃! u, π ^ (k + 1) ∣ u - t ∧ Polynomial.eval u f = 0
Lean
Formalized in Tau Ceti as TauCeti.IsAdicComplete.existsUnique_eval_eq_zero_of_dvd_pow.
Sources
Uses 1
TheoremHensel's lemma without monicity#
Over a Henselian pair (R, J), a simple root of a
polynomial modulo J lifts to a root with the same image in R ⧸ J, whether or not the polynomial
is monic.
Polynomial.exists_isRoot_sub_mem.{u_1} {R : Type u_1} [CommRing R] {J : Ideal R} [HenselianRing R J]
(f : Polynomial R) {a₀ : R} (h₁ : Polynomial.eval a₀ f ∈ J)
(h₂ : IsUnit ((Ideal.Quotient.mk J) (Polynomial.eval a₀ (Polynomial.derivative f)))) :
∃ a, f.IsRoot a ∧ a - a₀ ∈ J
Used by 4
TheoremJacobi's formula#
a derivation D differentiates the determinant of M as the trace of
the adjugate of M times the entrywise derivative of M.
Derivation.leibniz_det.{u_1, u_2, u_3} {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A]
[Algebra R A] (D : Derivation R A A) {n : Type u_3} [Fintype n] [DecidableEq n]
(M : Matrix n n A) : D M.det = (M.adjugate * M.map ⇑D).trace
TheoremThe Jacobian criterion for étaleness#
If T is smooth over R and the differentials
d aᵢ of finitely many elements aᵢ of T form a basis of Ω[T⁄R], then T is étale over the
polynomial ring R[Xᵢ] via Xᵢ ↦ aᵢ.
TauCeti.etale_aeval_of_basis.{u_1, u_3, u_4} {R : Type u_1} {T : Type u_3} [CommRing R] [CommRing T]
[Algebra R T] [Algebra.Smooth R T] {ι : Type u_4} [Finite ι] (a : ι → T)
(b : Module.Basis ι T Ω[T⁄R]) (hb : ∀ (i : ι), b i = (KaehlerDifferential.D R T) (a i)) :
(MvPolynomial.aeval a).Etale
Used by 12
[𝔤, x] · Borel conjugacy · Drinfeld and naive [Γ(N)]-structures coincide where N is invertible (Katz–Mazur, §3.7) · Multiplication by a nonzero integer n is an isogeny of degree n² · The integral moduli problem [Γ(N)] is relatively representable (Katz–Mazur, 3.6.0) · The n-torsion of an elliptic curve is étale where n is invertible (Katz–Mazur 2.3.1) · The Abel–Jacobi map into the degree-zero Picard fppf sheaf · The Abel–Jacobi map of a curve of positive genus separates points over every field extension · The degree-zero Picard functor Pic⁰_{X/S} · The points of an elliptic curve form Pic⁰ of its projective model
TheoremKedlaya's estimate (4.9.1) in the normalisation λ_ρ(p) = ρ#
Every
d ∈ 𝕎 O[1/(p [ϖ])] is a polynomial ∑_{i ≤ m} zᵢ p^(-(m - i)) in p⁻¹ whose coefficients zᵢ
lie in 𝕎 O[1/[ϖ]] and satisfy λ_{ρ₂}(zᵢ) ρ₁^(-(m - i)) ≤ λ_{[ρ₁, ρ₂]}(d). Writing
d = y / (p [ϖ]) ^ m and splitting y = ∑_{i < m} [yᵢ] pⁱ + pᵐ b, one takes zᵢ = [yᵢ] / [ϖ] ^ m
for i < m and zₘ = b / [ϖ] ^ m.
TauCeti.WittVector.IntervalLocalization.exists_sum_eq_mul_inv_pow.{u_1, u_2} (p : ℕ)
[Fact (Nat.Prime p)] {K : Type u_1} {O : Type u_2} [Field K] [CommRing O] [Algebra O K]
[CharP O p] [PerfectRing O p] {v : Valuation K NNReal} {ϖ : O} (hv : v.Integers O) (hϖ : ϖ ≠ 0)
(hϖ' : v ((algebraMap O K) ϖ) < 1) {ρ₁ ρ₂ : NNReal} (hρ₁ : ρ₁ ∈ Set.Ioo 0 1)
(hρ₂ : ρ₂ ∈ Set.Ioo 0 1) (d : TauCeti.WittVector.IntervalLocalization p hv hϖ hϖ' hρ₁ hρ₂) :
∃ m z,
(∀ i ≤ m, ‖z i‖ * (↑ρ₁)⁻¹ ^ (m - i) ≤ ‖d‖) ∧
d =
∑ i ∈ Finset.range (m + 1),
(TauCeti.WittVector.RadiusLocalization.toIntervalLocalization p hv hϖ hϖ' hρ₁ hρ₂) (z i) *
↑⋯.unit⁻¹ ^ (m - i)
Lean
Formalized in Tau Ceti as TauCeti.WittVector.IntervalLocalization.exists_sum_eq_mul_inv_pow.
Sources
Used by 1
TheoremKrull–Akizuki for Mathlib's integralClosure#
The specialisation of
TauCeti.IsIntegralClosure.isNoetherianRing to the integral closure of A in L as a
subalgebra.
TauCeti.integralClosure.isNoetherianRing.{u_1, u_2, u_3} {A : Type u_1} [CommRing A] [IsDomain A]
[IsNoetherianRing A] [Ring.KrullDimLE 1 A] {L : Type u_2} [CommRing L] [IsDomain L] [Algebra A L]
(K : Type u_3) [Field K] [Algebra A K] [IsFractionRing A K] [_root_.Module K L]
[IsScalarTower A K L] [Module.Finite K L] : IsNoetherianRing ↥(integralClosure A L)
Lean
Formalized in Tau Ceti as TauCeti.integralClosure.isNoetherianRing.
Other forms
Krull–Akizuki. Formalized in Tau Ceti as TauCeti.IsIntegralClosure.isNoetherianRing.
TauCeti.IsIntegralClosure.isNoetherianRing.{u_1, u_2, u_3, u_4} {A : Type u_1} [CommRing A]
[IsDomain A] [IsNoetherianRing A] [Ring.KrullDimLE 1 A] {L : Type u_2} [CommRing L] [IsDomain L]
[Algebra A L] (K : Type u_3) [Field K] [Algebra A K] [IsFractionRing A K] [_root_.Module K L]
[IsScalarTower A K L] [Module.Finite K L] (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C L]
[IsScalarTower A C L] [IsIntegralClosure C A L] : IsNoetherianRing C
Sources
Uses 1 · Used by 13
E[m] · The Wronskian identity of an isogeny · Isogenous curves over a finite field have the same zeta function Z(W/F, T) = exp (∑_{n ≥ 1} #W(𝔽_{qⁿ}) Tⁿ / n) · The φ-descent sequence is exact at H¹(G_K, E₁[φ]) · The Hasse bound (Silverman V.1.1) · The m-Selmer group of an elliptic curve over a number field is finite (Silverman X.4.2) · Serre duality on X_F, in dimensions · The Riemann–Roch theorem on X_F in dimension form · A curve of genus zero with a divisor of degree one has nodal reduction · The Abel–Jacobi map of a curve of positive genus separates points over every field extension · The anti-equivalence between regular proper curves and algebraic function fields over a field k · Kummer's theorem (Stichtenoth, Corollary 3.3.8) · The fundamental identityLoading dependency explorer…
The dependency explorer needs JavaScript and its graph data.