Module

FiniteAlgebraHom.lean

Nyll.AnabelianGeometry.WeightFiltration.FiniteAlgebraHom

1 declaration indexed from sourceView source ↗

Module documentation

Finite-valued points of a finitely generated algebra

A homomorphism is determined by its values on finitely many algebra generators. This gives the affine finiteness input for rational points over finite fields, without a zero-dimensional or module-finite hypothesis.

Imports1

Mathlib.RingTheory.FiniteType

Imported by2

theorem

finite_algHom_of_finiteType

L20 ↗

AnabelianGeometry.WeightFiltration.finite_algHom_of_finiteType

Documentation

A finite-type algebra has finitely many algebra maps to a finite algebra.

Source context 1 command

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

namespace AnabelianGeometry.WeightFiltration

Lean source · statement

theorem finite_algHom_of_finiteType
    (R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B]
    [Algebra R A] [Algebra R B] [Algebra.FiniteType R A] [Finite B] :
    Finite (A →ₐ[R] B)

Module documentation

Finite-valued points of a finitely generated algebra

Declarations

finite_algHom_of_finiteType