Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

a1_homotopy_type_ty

A1HomotopyType : Scheme → A1SpaceObj The A¹-homotopy type Sing^{A¹}(X) of an algebraic variety X.

abelian_variety_ty

AbelianVariety : Field → Nat → Type An abelian variety over a field k of dimension g is a smooth projective group variety.

absolute_height_ty

AbsoluteHeight : ProjectivePoint → Real H(P) = max|x_i|_v, the absolute Weil height on projective space.

adic_space_ty

AdicSpace : HuberRing → Type An adic space Spa(A, A+) for a Huber ring A, generalizing rigid analytic spaces.

affinoid_algebra_ty

AffinoidAlgebra : NonArchField → Type An affinoid algebra T_n/I over a non-archimedean field K.

analytic_ring_structure_ty

Analytic ring structure: every solid abelian group admits a natural analytic ring structure.

andre_oort_conjecture_ty

TolimaniConjecture : ShimuraVarietyObj → Prop The André-Oort conjecture: special subvarieties are Zariski closures of special points.

app

app2

app3

arrow

automorphic_representation_ty

AutomorphicRepresentation : ReductiveGroup → Type An automorphic representation π = ⊗_v π_v of a reductive group G over a number field.

beilinson_lichtenbaum_ty

Beilinson-Lichtenbaum conjecture (proved): motivic cohomology agrees with étale cohomology in the range p ≤ q (mod n).

berkovich_skeleton_retract_ty

Berkovich analytification is a retract onto the skeleton.

berkovich_space_ty

BerkovichSpace : AffinoidAlgebra → Type The Berkovich space M(A) of an affinoid algebra A: the space of bounded multiplicative seminorms.

bool_ty

bsd_conjecture_ty

BSD conjecture data: rank of E(ℚ) equals order of vanishing of L(E, s) at s=1.

build_env

Register all arithmetic geometry axioms and theorem types in the environment.

bvar

canonical_model_ty

CanonicalModel : ShimuraVarietyObj → ReflexField → AlgebraicVariety The canonical model of a Shimura variety over its reflex field E(G, X).

condensed_set_ty

CondensedSet : Type A condensed set is a sheaf of sets on the category of profinite sets (Clausen-Scholze).

crystalline_cohomology_ty

CrystallineCohomology : Scheme → Ring → AbelianGroup Crystalline cohomology H^i_{cris}(X/W) of a smooth proper variety in characteristic p.

crystalline_de_rham_iso_ty

Crystalline comparison theorem (Berthelot-Ogus): for a smooth proper scheme over W(k), H^i_{cris}(X_k/W(k)) ≅ H^i_{dR}(X/W(k)).

cst

diamond_ty

Diamond : PerfectoidSpaceObj → Type X^◇ = X / (Frobenius equivalence), the diamond associated to a perfectoid space.

dual_abelian_variety_ty

DualAbelianVariety : AbelianVarietyObj → AbelianVarietyObj A^ = Pic^0(A), the dual abelian variety (variety of degree-0 line bundles).

elliptic_curve_ty

EllipticCurve : Field → Type An elliptic curve E/k given by a Weierstrass equation y² = x³ + ax + b.

faltings_height_ty

FaltingsHeight : AbelianVarietyObj → Real The Faltings height h_F(A) of a principally polarized abelian variety A.

faltings_mordell_ty

Faltings’s theorem (Mordell conjecture, proved by Faltings 1983).

faltings_thm_ty

FaltingsThm : AlgebraicCurve → Prop Faltings’s theorem (Mordell conjecture): a curve of genus ≥ 2 over ℚ has finitely many rational points.

fontaine_de_rham_comparison_ty

Fontaine’s C_dR ⊗ D_dR(V) ≅ C_dR ⊗ V: de Rham comparison for p-adic representations.

fontaine_theory_ty

FontaineTheory : PAdicField → GaloisRepresentationObj → HodgeTateDecomp Fontaine’s theory associates a Hodge-Tate decomposition to a de Rham Galois representation.

galois_representation_ty

GaloisRepresentation : GaloisGroup → Nat → Ring → Type A continuous homomorphism ρ: G_K → GL_n(R).

global_langlands_ty

Global Langlands conjecture: correspondence between automorphic forms and Galois representations.

hasse_bound

Estimate the number of rational points on E(𝔽_q) using Hasse’s bound.

height_function_ty

HeightFunction : EllipticCurveObj → EllipticPointObj → Real The canonical Néron-Tate height ĥ: E(K̄) → ℝ.

int_ty

isogeny_theorem_ty

Isogeny theorem: for abelian varieties over finite fields, Hom(A, B) ⊗ ℤ_ℓ ≅ Hom(T_ℓ A, T_ℓ B).

isogeny_ty

Isogeny : EllipticCurveObj → EllipticCurveObj → Type A group homomorphism φ: E → E’ with finite kernel.

j_invariant

j-invariant of y² = x³ + ax + b (returns None if singular).

langlands_correspondence_ty

LanglandsCorrespondence : GaloisRepresentationObj → AutomorphicRepresentationObj → Prop The local/global Langlands correspondence: ρ_π ↔ π.

liquid_tensor_exact_ty

Liquid tensor product: the p-liquid tensor product is exact for 0 < p ≤ 1.

liquid_vector_space_ty

LiquidVectorSpace : Real → CondensedVectorSpaceObj → Prop A p-liquid vector space V is a condensed vector space satisfying the p-liquid condition.

list_ty

local_langlands_gl_n_ty

Local Langlands correspondence for GL_n.

log_crystalline_cohomology_ty

LogCrystallineCohomology : LogSchemeObj → Ring → AbelianGroup Log-crystalline cohomology H^i_{log-cris}(X/W) with W the Witt vectors.

log_etale_cohomology_ty

LogEtaleCohomology : LogSchemeObj → Nat → AbelianGroup Log-étale cohomology H^i_{log-et}(X, Z/nZ) of a log scheme X.

log_scheme_ty

LogScheme : Scheme → LogStructure → Type A log scheme (X, M_X) where M_X is a sheaf of monoids on X (Fontaine-Illusie-Kato).

logarithmic_height_ty

LogarithmicHeight : ProjectivePoint → Real h(P) = log H(P), the logarithmic Weil height.

mixed_motive_ty

MixedMotive : NumberField → Type A mixed motive over a number field K: an object in Voevodsky’s triangulated category of motives.

mordell_weil_ty

Mordell-Weil theorem: E(K) is a finitely generated abelian group.

motivic_chow_comparison_ty

Motivic cohomology comparison: H^{2n,n}(X, Z) ≅ CH^n(X) (Chow groups).

motivic_cohomology_ty

MotivicCohomology : Scheme → Int → Int → AbelianGroup Motivic cohomology H^{p,q}(X, Z), the bigraded cohomology theory of algebraic varieties.

nat_ty

nearly_ordinary_representation_ty

NearlyOrdinaryRepresentation : GaloisGroup → Prime → Type A p-adic Galois representation admitting a Borel reduction at p (ordinary at p).

neron_mapping_property_ty

Néron mapping property: every rational map from a smooth scheme to A extends to N(A).

neron_model_ty

NeronModel : AbelianVarietyObj → DVRing → GroupScheme The Néron model N(A) of an abelian variety A over the fraction field of a DVR.

neron_tate_parallelogram_ty

Néron-Tate height satisfies the parallelogram law.

northcott_faltings_height_ty

Northcott for Faltings heights: there are finitely many isomorphism classes of principally polarized abelian varieties over K with bounded Faltings height and fixed dimension.

northcott_projective_ty

Northcott property for projective space.

northcott_property_ty

NorthcottProperty : Type → Prop A set S has the Northcott property if for all B, {P ∈ S : H(P) ≤ B} is finite.

perfectoid_space_ty

PerfectoidSpace : Type A perfectoid space is a topological space with a perfectoid algebra structure, used to transfer problems between characteristic 0 and characteristic p.

pi

poincare_reducibility_ty

Poincaré reducibility: every abelian variety is isogenous to a product of simple abelian varieties.

polarized_abelian_variety_ty

PolarizedAbelianVariety : Field → Nat → Type An abelian variety together with an ample line bundle (polarization).

prismatic_cohomology_ty

PrismaticCohomology : Scheme → Prism → AbelianGroup The prismatic cohomology H^*_{Δ}(X/A) of a p-adic formal scheme X over a prism (A, I).

prismatic_comparison_ty

Prismatic comparison: prismatic cohomology specializes to de Rham, étale, and crystalline cohomology.

pro_etale_comparison_ty

Pro-étale cohomology: the pro-étale cohomology of X with coefficients in Z_ℓ.

pro_etale_topos_ty

ProEtaleTopos : Scheme → Topos The pro-étale topos X_{pro-ét} of a scheme X (Bhatt-Scholze).

prop

rank_lower_bound_2descent

Compute the rank of an elliptic curve E/ℚ via naive 2-descent lower bound.

real_ty

rigid_analytic_space_ty

RigidAnalyticSpace : NonArchField → Type A rigid analytic space (Tate, 1971) over a non-archimedean field.

rigid_gaga_ty

GAGA for rigid analytic spaces: coherent analytic sheaves correspond to algebraic coherent sheaves.

sato_tate_ty

Sato-Tate conjecture: for a non-CM elliptic curve E/ℚ, the distribution of a_p / 2√p is equidistributed with respect to the Sato-Tate measure on [-1, 1].

semi_stable_reduction_ty

Semi-stable reduction theorem: after a finite base change, any abelian variety becomes semi-stable.

shimura_datum_ty

ShimuraDatum : ReductiveGroup → HermitianDomain → Type A Shimura datum (G, X) where G is a reductive group and X a hermitian symmetric domain.

shimura_reciprocity_ty

Reciprocity law for Shimura varieties: Frobenius acts on special points via the reflex norm.

shimura_variety_ty

ShimuraVariety : ShimuraDatumObj → CompactOpenSubgroup → Type Sh_K(G, X) = G(ℚ) \ X × G(𝔸_f) / K, a moduli space of abelian varieties with extra structure.

slice_filtration_ty

SliceFiltration : MotiveObj → Nat → MotiveObj Voevodsky’s slice filtration s_n(M): the n-th slice of a motive M.

solid_abelian_group_ty

SolidAbelianGroup : CondensedAbelianGroupObj → Prop A condensed abelian group is solid if it satisfies the solid module condition (Clausen-Scholze).

syntomic_cohomology_ty

Syntomic Cohomology : Scheme → Nat → AbelianGroup Syntomic cohomology H^i_{syn}(X, Z_p(n)), interpolating between crystalline and étale.

tate_module_rank_ty

Tate module rank theorem.

tate_module_ty

TateModule : AbelianVarietyObj → Prime → ZpModule T_p(A) = lim_{n} A[p^n], the p-adic Tate module of A, free of rank 2g over ℤ_p.

tilting_equivalence_ty

Tilting equivalence: there is an equivalence between perfectoid spaces of characteristic 0 and characteristic p via the tilt functor X ↦ X^♭.

torsion_point_ty

TorsionPoint : EllipticCurveObj → Nat → Type E[n] = {P ∈ E : nP = O}, the n-torsion subgroup.

torsion_structure_ty

Torsion structure: E[n] ≅ (ℤ/nℤ)² over an algebraically closed field of characteristic 0.

type0

type1

v_stack_ty

VStack : Site → Type A v-stack (sheaf on the v-topology), generalizing perfectoid spaces and diamonds.

voevodsky_cancellation_ty

Voevodsky’s cancellation theorem: ⊗ A¹ is invertible in the motivic stable homotopy category.

weierstrass_discriminant

Discriminant of a Weierstrass cubic y² = x³ + ax + b.

weil_pairing_ty

Weil pairing: E[n] × E^[n] → μ_n (alternating, non-degenerate).