ModuleEtaleFieldPointBound.lean
Nyll.SchemeTheory.RingTheory.EtaleFieldPointBound
2 declarations indexed from sourceView source ↗ Module documentation
Uniform bounds for field-valued points on étale charts
Maps from a standard étale algebra to a field inject into the roots of its defining monic polynomial. The existing standard-étale hom equivalence and root-cardinality theorem therefore give actual finiteness and a numerical bound independent of the target field and of its algebra structure.
The local structure theorem supplies such a principal chart at every prime of an arbitrary étale algebra. The chart and bound are chosen before the target field. No tensor-product decomposition or assumed fiber comparison is introduced. Finite-cover aggregation and conversion to cardinalities of scheme-theoretic geometric fibers remain subsequent steps toward 09Z0.
Imports5
- Mathlib.Algebra.Algebra.Equiv
- Mathlib.Algebra.Polynomial.Roots
- Mathlib.RingTheory.Etale.StandardEtale
- Mathlib.RingTheory.Unramified.LocalStructure
- Mathlib.SetTheory.Cardinal.Finite
Imported by2
Declarations
StandardEtalePair.fieldHom_finite_and_card_le
DocumentationField-valued points of a standard étale algebra form a finite set of cardinality at most the degree of its defining monic polynomial.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
namespace StandardEtalePair
Algebra.Etale.exists_local_uniform_fieldHom_bound
DocumentationEvery prime of an étale algebra has a principal neighborhood with a finite bound on all field-valued points. Both the neighborhood and the bound are independent of the field and its map from the base ring.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
namespace Algebra.Etale