Scheme, stack, cohomology and intersection foundations
The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.
TheoremThe henselization of a pair is henselian#
The pair formed by the henselization of
(R, I) and the extended ideal is a henselian pair, with no hypothesis on R or I.
TauCeti.Henselization.henselian.{u} {R : Type u} [CommRing R] (I : Ideal R) :
HenselianRing (↑(TauCeti.Henselization.algebra I)) (TauCeti.Henselization.extended I)
TheoremThe universal property of the henselization#
For a henselian pair (S, J) receiving a
map of pairs from (R, I), there is a unique R-algebra map from the henselization of
(R, I) to S carrying the extended ideal into J.
TauCeti.Henselization.existsUnique_lift.{u, v} {R : Type u} [CommRing R] {I : Ideal R} {S : Type v}
[CommRing S] [Algebra R S] (J : Ideal S) [HenselianRing S J]
(hIJ : Ideal.map (algebraMap R S) I ≤ J) :
∃! f, Ideal.map f (TauCeti.Henselization.extended I) ≤ J
TheoremThe universal property of the henselization of a local ring#
Every local homomorphism
from a local ring R to a henselian local ring S factors through a unique local
R-algebra map from the henselization of R along its maximal ideal. Every R-algebra map
from the henselization to S is in fact local and equal to this one (eq_lift).
TauCeti.Henselization.existsUnique_isLocalHom.{u, v} {R : Type u} [CommRing R] [IsLocalRing R]
{S : Type v} [CommRing S] [HenselianLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] :
∃! f, IsLocalHom f
TheoremResolution of curves: regularity of the normalization#
Let Y be an integral locally
Noetherian scheme of dimension at most one, and suppose that the normalization of Y in its
function field, along Spec k(Y) ⟶ Y, is finite over Y. Then this normalization is a regular
scheme.
TauCeti.AlgebraicGeometry.isRegular_normalization_fromSpecStalk_genericPoint.{u}
{Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral Y]
[AlgebraicGeometry.IsLocallyNoetherian Y] (hY : topologicalKrullDim ↥Y ≤ 1)
[AlgebraicGeometry.IsFinite
(AlgebraicGeometry.Scheme.Hom.fromNormalization (Y.fromSpecStalk (genericPoint ↥Y)))] :
TauCeti.AlgebraicGeometry.IsRegular
(AlgebraicGeometry.Scheme.Hom.normalization (Y.fromSpecStalk (genericPoint ↥Y)))
Lean
Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.isRegular_normalization_fromSpecStalk_genericPoint.
Sources
- Tau Ceti documentation:
TauCeti.AlgebraicGeometry.isRegular_normalization_fromSpecStalk_genericPoint - Source of
TauCeti.AlgebraicGeometry.isRegular_normalization_fromSpecStalk_genericPointin TauCeti/AlgebraicGeometry/Normalization/Regular.lean - Tau Ceti roadmap status: Scheme, stack, cohomology and intersection foundations
TheoremResolution of curves: the normalization is a modification#
If the normalization of an
integral scheme Y in its function field, along Spec k(Y) ⟶ Y, is finite over Y, then it is a
modification of Y: it is proper, and an isomorphism over a dense open of Y with dense preimage.
Stacks, Lemma 33.41.1 (0C45) over a field.
TauCeti.AlgebraicGeometry.isModification_fromNormalization_fromSpecStalk_genericPoint.{u}
{Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral Y]
[AlgebraicGeometry.IsFinite
(AlgebraicGeometry.Scheme.Hom.fromNormalization (Y.fromSpecStalk (genericPoint ↥Y)))] :
TauCeti.AlgebraicGeometry.IsModification
(AlgebraicGeometry.Scheme.Hom.fromNormalization (Y.fromSpecStalk (genericPoint ↥Y)))
Lean
Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.isModification_fromNormalization_fromSpecStalk_genericPoint.
Sources
- Tau Ceti documentation:
TauCeti.AlgebraicGeometry.isModification_fromNormalization_fromSpecStalk_genericPoint - Source of
TauCeti.AlgebraicGeometry.isModification_fromNormalization_fromSpecStalk_genericPointin TauCeti/AlgebraicGeometry/Normalization/Modification.lean - Tau Ceti roadmap status: Scheme, stack, cohomology and intersection foundations
TheoremZariski's main theorem, global form#
A quasi-finite algebra A of finite type over R
has a module-finite subalgebra A' and finitely many elements r ∈ A' generating the unit ideal
of A, such that for every x ∈ A and every such r, all large enough powers of r move x
into A'. Geometrically, Spec A is covered by finitely many basic opens D(r) on which it
agrees with the finite R-scheme Spec A'.
Algebra.QuasiFinite.exists_fg_subalgebra_and_span_eq_top.{u_1, u_2} {R : Type u_1} {A : Type u_2}
[CommRing R] [CommRing A] [Algebra R A] [Algebra.FiniteType R A] [Algebra.QuasiFinite R A] :
∃ A' s,
(Subalgebra.toSubmodule A').FG ∧
↑s ⊆ ↑A' ∧ Ideal.span ↑s = ⊤ ∧ ∀ r ∈ s, ∀ (x : A), ∀ᶠ (m : ℕ) in Filter.atTop, r ^ m * x ∈ A'
Lean
Formalized in Tau Ceti as Algebra.QuasiFinite.exists_fg_subalgebra_and_span_eq_top.
Sources
TheoremThe absolute Frobenius is a universal homeomorphism#
every base change of F_X is a
homeomorphism of underlying spaces.
AlgebraicGeometry.Scheme.universally_isHomeomorph_frobenius.{u} {X : AlgebraicGeometry.Scheme}
{p : ℕ} [Fact (Nat.Prime p)] (hX : ↑p = 0) :
(AlgebraicGeometry.topologically @IsHomeomorph).universally (X.frobenius p hX)
Lean
Formalized in Tau Ceti as AlgebraicGeometry.Scheme.universally_isHomeomorph_frobenius.
Sources
- Tau Ceti documentation:
AlgebraicGeometry.Scheme.universally_isHomeomorph_frobenius - Source of
AlgebraicGeometry.Scheme.universally_isHomeomorph_frobeniusin TauCeti/AlgebraicGeometry/Frobenius/UniversalHomeomorphism.lean - Tau Ceti roadmap status: Scheme, stack, cohomology and intersection foundations
TheoremThe absolute Frobenius of a scheme locally of finite type over a perfect ring is finite#
For a scheme X locally of finite type over Spec R, with R a perfect ring of characteristic
p, the absolute Frobenius F_X : X ⟶ X is a finite morphism.
AlgebraicGeometry.Scheme.isFinite_frobenius.{u} {X : AlgebraicGeometry.Scheme} {p : ℕ}
[Fact (Nat.Prime p)] {R : Type u} [CommRing R] [ExpChar R p] [PerfectRing R p]
(f : X ⟶ AlgebraicGeometry.Spec ↧R) [AlgebraicGeometry.LocallyOfFiniteType f] (hX : ↑p = 0) :
AlgebraicGeometry.IsFinite (X.frobenius p hX)
ClassTauCeti.Ring.IsJapanese#
A domain R is Japanese (or N-2) if for every finite extension L of its fraction field,
the integral closure of R in L is a finite R-module; inseparable extensions are included.
Stacks, Definition 10.161.1 (032F). See IsJapanese.finite_integralClosure for an arbitrary model
of the fraction field and an extension in an arbitrary universe.
TauCeti.Ring.IsJapanese.{u} (R : Type u) [CommRing R] [IsDomain R] : Prop
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 · The fundamental identity · TauCeti.Ring.IsNagataClassTauCeti.Ring.IsNagata#
A commutative ring R is Nagata if it is Noetherian and the quotient R ⧸ p by every prime
ideal p is a Japanese domain. Stacks, Definition 10.162.1 (032R).
TauCeti.Ring.IsNagata.{u} (R : Type u) [CommRing R] : Prop
Uses 1
DefinitionModule.SatisfiesSerreS#
An R-module M satisfies Serre's condition (S_n) if for every prime p of R the depth
of M_p over R_p is at least min (n, dim Supp M_p). This is meant for finite modules over a
Noetherian ring. Since the zero module has depth ⊤, primes outside the support impose nothing.
Stacks, Definition 10.157.1 (031P).
Module.SatisfiesSerreS.{u, v} (n : ℕ) (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M]
[_root_.Module R M] : Prop
Used by 1
DefinitionRing.SatisfiesSerreR#
A ring R satisfies Serre's condition (R_n) if every prime of height at most n lies in
the regular locus, that is, R_p is a regular local ring whenever ht p ≤ n. Stacks,
Definition 10.157.1 (031P).
Ring.SatisfiesSerreR.{u} (n : ℕ) (R : Type u) [CommRing R] : Prop
Used by 1
ClassTauCeti.Excellence.GeometricallyRegular#
An algebra B over a field k is geometrically regular if B is Noetherian and
L ⊗[k] B is a regular ring for every finite purely inseparable field extension L / k
(Stacks, Definition 10.166.2, in the form of Lemma 10.166.1). The extensions L range over the
universe of k; GeometricallyRegular.isRegularRing_tensorProduct' removes that restriction.
TauCeti.Excellence.GeometricallyRegular.{u, v} (k : Type u) (B : Type v) [Field k] [CommRing B]
[Algebra k B] : Prop
Used by 1
ClassTauCeti.Excellence.RegularAlgebraMap#
An R-algebra B is a regular algebra, or R → B is a regular ring map, if B is flat
over R and for every prime p of R the fibre κ(p) ⊗[R] B is geometrically regular over the
residue field κ(p) (Stacks, Definition 15.42.1).
TauCeti.Excellence.RegularAlgebraMap.{u, v} (R : Type u) (B : Type v) [CommRing R] [CommRing B]
[Algebra R B] : Prop
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.