Documentation

TauCeti.Topology.Algebra.PointTopology.Basic

The point topology on points of an affine algebra #

Let A be a k-algebra and R a topological k-algebra. The R-points of the affine scheme Spec A over k are the k-algebra homomorphisms A →ₐ[k] R. Their point topology is the coarsest topology making every evaluation x ↦ x a continuous, that is, the topology induced from the product topology on A → R. No finiteness or separation hypothesis is needed to define it. For an affine group scheme, whose points carry the convolution group structure on WithConv (A →ₐ[k] R), the topology is transported along WithConv.ofConv; this is the topology on rational points used for topological groups of points over local fields and adeles.

When A is generated by a family a : ι → A, evaluation at that family embeds the points in ι → R, and for R a commutative ring with closed points the image is the closed common zero locus of the polynomial relations among the generators. So the point topology is the topology induced by any presentation of A. Taking all of A as the generating family shows that the points are compact when R is compact and T1. For A of finite type this gives local compactness when R is locally compact, and discreteness when R is discrete; without finite type discreteness fails, already for the points of a polynomial ring in infinitely many variables over 𝔽₂.

Mathlib's CommRingCat.HomTopology (Andrew Yang and Christian Merten) puts the same evaluation topology on ring homomorphisms A ⟶ R between bundled commutative rings, that is, on points over ℤ; the closed-embedding argument here follows its CommRingCat.HomTopology.isClosedEmbedding_precomp_of_surjective. The points of an affine scheme over a base k are instead k-algebra homomorphisms, which is the form in which affine group schemes over k and their convolution groups of points are set up.

Main declarations #

References #

source
@[implicit_reducible]
def TauCeti.PointTopology.topology {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Semiring R] [Algebra k R] [TopologicalSpace R] :
TopologicalSpace (A →ₐ[k] R)

The point topology on the R-points A →ₐ[k] R of Spec A: the coarsest topology for which every evaluation x ↦ x a is continuous, induced from the product topology on A → R. It is a scoped instance in the namespace TauCeti.PointTopology.

Instances For
    source
    theorem TauCeti.PointTopology.topology_eq_induced {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Semiring R] [Algebra k R] [TopologicalSpace R] :
    topology = TopologicalSpace.induced (fun (x : A →ₐ[k] R) => ⇑x) Pi.topologicalSpace

    The point topology is the topology induced from the product topology on A → R.

    source
    theorem TauCeti.PointTopology.isEmbedding_coeFn {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Semiring R] [Algebra k R] [TopologicalSpace R] :
    Topology.IsEmbedding fun (x : A →ₐ[k] R) => ⇑x

    Forgetting that a point is an algebra homomorphism embeds the points in A → R.

    source
    theorem TauCeti.PointTopology.continuous_eval {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Semiring R] [Algebra k R] [TopologicalSpace R] (a : A) :
    Continuous fun (x : A →ₐ[k] R) => x a

    Evaluation of points at an element of A is continuous.

    source
    theorem TauCeti.PointTopology.continuous_iff {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Semiring R] [Algebra k R] [TopologicalSpace R] {X : Type u_4} [TopologicalSpace X] {g : X → A →ₐ[k] R} :
    Continuous g ↔ ∀ (a : A), Continuous fun (y : X) => (g y) a

    A map into the points is continuous exactly when its composite with every evaluation is.

    source
    @[instance_reducible]
    instance TauCeti.PointTopology.instTopologicalSpaceWithConv {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Semiring R] [Algebra k R] [TopologicalSpace R] :
    TopologicalSpace (WithConv (A →ₐ[k] R))

    The point topology on the convolution type WithConv (A →ₐ[k] R), which carries the group of points of an affine group scheme: the topology transported from A →ₐ[k] R along WithConv.ofConv.

    source
    theorem TauCeti.PointTopology.isHomeomorph_ofConv {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Semiring R] [Algebra k R] [TopologicalSpace R] :
    IsHomeomorph WithConv.ofConv

    WithConv.ofConv is a homeomorphism from WithConv (A →ₐ[k] R) onto the points with their point topology.

    source
    theorem TauCeti.PointTopology.continuous_withConv_iff {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Semiring R] [Algebra k R] [TopologicalSpace R] {X : Type u_4} [TopologicalSpace X] {g : X → WithConv (A →ₐ[k] R)} :
    Continuous g ↔ ∀ (a : A), Continuous fun (y : X) => (g y).ofConv a

    A map into WithConv (A →ₐ[k] R) is continuous exactly when its composite with every evaluation is.

    source
    theorem TauCeti.PointTopology.continuous_eval_ofConv {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Semiring R] [Algebra k R] [TopologicalSpace R] (a : A) :
    Continuous fun (x : WithConv (A →ₐ[k] R)) => x.ofConv a

    Evaluation at a is continuous on WithConv (A →ₐ[k] R).

    source
    noncomputable def TauCeti.PointTopology.polynomialHomeomorph (k : Type u_1) (R : Type u_3) [CommSemiring k] [Semiring R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] :
    (Polynomial k →ₐ[k] R) ≃ₜ R

    The points of the affine line: evaluation at the variable is a homeomorphism from k[X] →ₐ[k] R onto R, with inverse r ↦ Polynomial.aeval r.

    Instances For
      source
      @[simp]
      theorem TauCeti.PointTopology.polynomialHomeomorph_apply {k : Type u_1} {R : Type u_3} [CommSemiring k] [Semiring R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] (x : Polynomial k →ₐ[k] R) :
      (polynomialHomeomorph k R) x = x Polynomial.X

      The homeomorphism polynomialHomeomorph evaluates a point at the variable.

      source
      @[simp]
      theorem TauCeti.PointTopology.polynomialHomeomorph_symm_apply {k : Type u_1} {R : Type u_3} [CommSemiring k] [Semiring R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] (r : R) :
      (polynomialHomeomorph k R).symm r = Polynomial.aeval r

      The inverse of polynomialHomeomorph sends r to evaluation at r.

      source
      noncomputable def TauCeti.PointTopology.mvPolynomialHomeomorph (k : Type u_1) (R : Type u_3) [CommSemiring k] [CommSemiring R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] (σ : Type u_4) :
      (MvPolynomial σ k →ₐ[k] R) ≃ₜ (σ → R)

      The points of affine space with coordinates indexed by σ: evaluation at the variables is a homeomorphism from MvPolynomial σ k →ₐ[k] R onto σ → R, with inverse MvPolynomial.aeval.

      Instances For
        source
        @[simp]
        theorem TauCeti.PointTopology.mvPolynomialHomeomorph_apply {k : Type u_1} {R : Type u_3} [CommSemiring k] [CommSemiring R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] {σ : Type u_4} (x : MvPolynomial σ k →ₐ[k] R) (i : σ) :
        (mvPolynomialHomeomorph k R σ) x i = x (MvPolynomial.X i)

        The homeomorphism mvPolynomialHomeomorph evaluates a point at each variable.

        source
        @[simp]
        theorem TauCeti.PointTopology.mvPolynomialHomeomorph_symm_apply {k : Type u_1} {R : Type u_3} [CommSemiring k] [CommSemiring R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] {σ : Type u_4} (v : σ → R) :
        (mvPolynomialHomeomorph k R σ).symm v = MvPolynomial.aeval v

        The inverse of mvPolynomialHomeomorph sends v to evaluation at v.

        source
        theorem TauCeti.PointTopology.isEmbedding_eval_generators {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [CommSemiring A] [Algebra k A] [CommSemiring R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] {ι : Type u_4} {a : ι → A} (ha : Algebra.adjoin k (Set.range a) = ⊤) :
        Topology.IsEmbedding fun (x : A →ₐ[k] R) (i : ι) => x (a i)

        If the family a generates A as a k-algebra, then evaluation at a embeds the points A →ₐ[k] R in ι → R.

        source
        theorem TauCeti.PointTopology.discreteTopology_of_finiteType {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [CommSemiring A] [Algebra k A] [CommSemiring R] [Algebra k R] [TopologicalSpace R] [DiscreteTopology R] [Algebra.FiniteType k A] :
        DiscreteTopology (A →ₐ[k] R)

        Points of a finite type algebra over a discrete coefficient ring form a discrete space.

        source
        theorem TauCeti.PointTopology.not_discreteTopology_mvPolynomial {k : Type u_1} {R : Type u_3} [CommSemiring k] [CommSemiring R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] (σ : Type u_4) [Infinite σ] [Nontrivial R] :
        ¬DiscreteTopology (MvPolynomial σ k →ₐ[k] R)

        Without finite type, points over a discrete ring need not be discrete: for infinitely many variables and a nontrivial coefficient ring, such as 𝔽₂ with the discrete topology, the points of affine space are not discrete, since every basic open set constrains only finitely many coordinates.

        source
        theorem TauCeti.PointTopology.range_eval_generators {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommRing k] [CommRing A] [Algebra k A] [CommRing R] [Algebra k R] {ι : Type u_4} {a : ι → A} (ha : Algebra.adjoin k (Set.range a) = ⊤) :
        (Set.range fun (x : A →ₐ[k] R) (i : ι) => x (a i)) = {v : ι → R | ∀ p ∈ RingHom.ker (MvPolynomial.aeval a), (MvPolynomial.aeval v) p = 0}

        For a family a generating A, the values of the points of A on a are exactly the families in ι → R at which every polynomial relation among the generators vanishes.

        source
        theorem TauCeti.PointTopology.isClosedEmbedding_eval_generators {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommRing k] [CommRing A] [Algebra k A] [CommRing R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] [T1Space R] {ι : Type u_4} {a : ι → A} (ha : Algebra.adjoin k (Set.range a) = ⊤) :
        Topology.IsClosedEmbedding fun (x : A →ₐ[k] R) (i : ι) => x (a i)

        If the family a generates A and R is T1, evaluation at a is a closed embedding of the points A →ₐ[k] R in ι → R, onto the common zero locus of the relations among the generators.

        source
        theorem TauCeti.PointTopology.locallyCompactSpace_of_finiteType {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommRing k] [CommRing A] [Algebra k A] [CommRing R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] [T1Space R] [LocallyCompactSpace R] [Algebra.FiniteType k A] :
        LocallyCompactSpace (A →ₐ[k] R)

        Points of a finite type algebra over a locally compact T1 coefficient ring form a locally compact space.

        source
        instance TauCeti.PointTopology.instCompactSpace {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommRing k] [CommRing A] [Algebra k A] [CommRing R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] [T1Space R] [CompactSpace R] :
        CompactSpace (A →ₐ[k] R)

        Points over a compact T1 coefficient ring form a compact space, with no finiteness hypothesis on A.

        source
        instance TauCeti.PointTopology.instCompactSpaceWithConv {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommRing k] [CommRing A] [Algebra k A] [CommRing R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] [T1Space R] [CompactSpace R] :
        CompactSpace (WithConv (A →ₐ[k] R))

        The convolution type WithConv (A →ₐ[k] R) is compact for a compact T1 coefficient ring.