Module

EtaleFieldPointGlobalBound.lean

Nyll.SchemeTheory.RingTheory.EtaleFieldPointGlobalBound

1 declaration indexed from sourceView source ↗

Module documentation

A global uniform bound for field-valued points of an étale algebra

Compactness of the actual prime spectrum gives a finite family of the previously constructed bounded principal charts. A map to a field has a prime kernel, so one chart element maps to a unit and the map extends by the existing localization lift. Restriction from the disjoint union of chart hom sets is therefore surjective. Their finite cardinalities add, giving one finite bound chosen before the target field and base map.

No nontriviality assumption on either algebra is required. Comparison with scheme-theoretic geometric fibers remains a separate step toward 09Z0.

Imports8

Nyll.SchemeTheory.RingTheory.EtaleFieldPointBound
Mathlib.Algebra.Algebra.Tower
Mathlib.Algebra.Order.BigOperators.Group.Finset
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.SetTheory.Cardinal.Finite
Mathlib.Topology.Compactness.Compact

Imported by2

theorem

exists_uniform_fieldHom_bound

L39 ↗

Algebra.Etale.exists_uniform_fieldHom_bound

Documentation

An étale algebra has a single finite bound on its field-valued points, uniform over all fields in the target universe and all base-ring maps.

Source context 3 commands

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

noncomputable section
universe u v w
namespace Algebra.Etale

Lean source · statement

theorem exists_uniform_fieldHom_bound
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Etale R S] :
    ∃ N : ℕ, ∀ (K : Type w) [Field K] [Algebra R K],
      Finite (S →ₐ[R] K) ∧ Nat.card (S →ₐ[R] K) ≤ N

Module documentation

A global uniform bound for field-valued points of an étale algebra

Declarations

exists_uniform_fieldHom_bound