NYLL
Module

FiniteAffinePoints.lean

Nyll.AnabelianGeometry.WeightFiltration.FiniteAffinePoints
1 declaration indexed from sourceView source ↗

Module documentation

Finiteness of actual affine points over finite rings

This is finiteness of morphisms over the base, not finiteness of the underlying topological fiber. The affine scheme may have positive dimension.

Imports3
Imported by1

Declarations

theorem

finite_affine_points

L24 ↗
AnabelianGeometry.WeightFiltration.finite_affine_points
Documentation

The actual finite-valued points of a finite-type affine scheme form a finite type, by the spectrum/algebra-homomorphism equivalence.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open AlgebraicGeometry CategoryTheory NeronModelInfra
namespace AnabelianGeometry.WeightFiltration
Lean source · statement
theorem finite_affine_points
    (R A B : Type) [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B] [Algebra.FiniteType R A] [Finite B] :
    Finite (SchemeHomOver (Spec.algebraMap R B) (Spec.algebraMap R A))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.