Documentation

Mathlib.Algebra.Category.Ring.Topology

Topology on Hom(R, S) #

In this file, we define topology on Hom(A, R) for a topological ring R, given by the coarsest topology that makes f ↦ f x continuous for all x : A. Alternatively, given a presentation A = ℤ[xᵢ]/I, this is the subspace topology Hom(A, R) ↪ Hom(ℤ[xᵢ], R) = Rᶥ.

Main results #

source
def CommRingCat.HomTopology.instTopologicalSpaceHom {R A : CommRingCat} [TopologicalSpace ↑R] :
TopologicalSpace (A ⟶ R)

The topology on Hom(A, R) for a topological ring R, given by the coarsest topology that makes f ↦ f x continuous for all x : A (see continuous_apply). Alternatively, given a presentation A = ℤ[xᵢ]/I, this is the subspace topology Hom(A, R) ↪ Hom(ℤ[xᵢ], R) = Rᶥ (see mvPolynomialHomeomorph).

This is a scoped instance in CommRingCat.HomTopology.

Equations
    Instances For
      source
      theorem CommRingCat.HomTopology.continuous_apply {R A : CommRingCat} [TopologicalSpace ↑R] (x : ↑A) :
      Continuous fun (f : A ⟶ R) => (Hom.hom f) x
      source
      theorem CommRingCat.HomTopology.isEmbedding_hom (R A : CommRingCat) [TopologicalSpace ↑R] :
      Topology.IsEmbedding fun (f : A ⟶ R) => ⇑(Hom.hom f)
      source
      theorem CommRingCat.HomTopology.continuous_precomp {R A B : CommRingCat} [TopologicalSpace ↑R] (f : A ⟶ B) :
      Continuous fun (x : B ⟶ R) => CategoryTheory.CategoryStruct.comp f x
      source
      def CommRingCat.HomTopology.precompHomeomorph {R A B : CommRingCat} [TopologicalSpace ↑R] (f : A ≅ B) :
      (B ⟶ R) ≃ₜ (A ⟶ R)

      If A ≅ B, then Hom(A, R) is homeomorphic to Hom(B, R).

      Equations
        Instances For
          source
          @[simp]
          theorem CommRingCat.HomTopology.precompHomeomorph_apply {R A B : CommRingCat} [TopologicalSpace ↑R] (f : A ≅ B) (φ : B ⟶ R) :
          (precompHomeomorph f) φ = CategoryTheory.CategoryStruct.comp f.hom φ
          source
          @[simp]
          theorem CommRingCat.HomTopology.precompHomeomorph_symm_apply {R A B : CommRingCat} [TopologicalSpace ↑R] (f : A ≅ B) (φ : A ⟶ R) :
          (precompHomeomorph f).symm φ = CategoryTheory.CategoryStruct.comp f.inv φ
          source
          theorem CommRingCat.HomTopology.isHomeomorph_precomp {R A B : CommRingCat} [TopologicalSpace ↑R] (f : A ⟶ B) [CategoryTheory.IsIso f] :
          IsHomeomorph fun (x : B ⟶ R) => CategoryTheory.CategoryStruct.comp f x
          source
          theorem CommRingCat.HomTopology.isEmbedding_precomp_of_surjective {R A B : CommRingCat} [TopologicalSpace ↑R] (f : A ⟶ B) (hf : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) :
          Topology.IsEmbedding fun (x : B ⟶ R) => CategoryTheory.CategoryStruct.comp f x

          Hom(A/I, R) has the subspace topology of Hom(A, R). More generally, a surjection A ⟶ B gives rise to an embedding Hom(B, R) ⟶ Hom(A, R)

          source
          theorem CommRingCat.HomTopology.isClosedEmbedding_precomp_of_surjective {R A B : CommRingCat} [TopologicalSpace ↑R] [T1Space ↑R] (f : A ⟶ B) (hf : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) :
          Topology.IsClosedEmbedding fun (x : B ⟶ R) => CategoryTheory.CategoryStruct.comp f x

          Hom(A/I, R) is a closed subspace of Hom(A, R) if R is T1.

          source
          noncomputable def CommRingCat.HomTopology.mvPolynomialHomeomorph (σ : Type v) (R A : CommRingCat) [TopologicalSpace ↑R] [IsTopologicalRing ↑R] :
          (of (MvPolynomial σ ↑A) ⟶ R) ≃ₜ (A ⟶ R) × (σ → ↑R)

          Hom(A[Xᵢ], R) is homeomorphic to Hom(A, R) × Rⁱ.

          Equations
            Instances For
              source
              @[simp]
              theorem CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_snd (σ : Type v) (R A : CommRingCat) [TopologicalSpace ↑R] [IsTopologicalRing ↑R] (f : of (MvPolynomial σ ↑A) ⟶ R) (i : σ) :
              ((mvPolynomialHomeomorph σ R A) f).2 i = (CategoryTheory.ConcreteCategory.hom f) (MvPolynomial.X i)
              source
              @[simp]
              theorem CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_fst (σ : Type v) (R A : CommRingCat) [TopologicalSpace ↑R] [IsTopologicalRing ↑R] (f : of (MvPolynomial σ ↑A) ⟶ R) :
              ((mvPolynomialHomeomorph σ R A) f).1 = CategoryTheory.CategoryStruct.comp (ofHom MvPolynomial.C) f
              source
              @[simp]
              theorem CommRingCat.HomTopology.mvPolynomialHomeomorph_symm_apply_hom (σ : Type v) (R A : CommRingCat) [TopologicalSpace ↑R] [IsTopologicalRing ↑R] (fx : (A ⟶ R) × (σ → ↑R)) :
              Hom.hom ((mvPolynomialHomeomorph σ R A).symm fx) = MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2
              source
              theorem CommRingCat.HomTopology.isClosedEmbedding_hom (R A : CommRingCat) [TopologicalSpace ↑R] [IsTopologicalRing ↑R] [T1Space ↑R] :
              Topology.IsClosedEmbedding fun (f : A ⟶ R) => ⇑(Hom.hom f)
              source
              instance CommRingCat.HomTopology.instT2SpaceHomOfCarrier {R A : CommRingCat} [TopologicalSpace ↑R] [T2Space ↑R] :
              T2Space (A ⟶ R)
              source
              instance CommRingCat.HomTopology.instCompactSpaceHomOfIsTopologicalRingOfT1SpaceOfCarrier {R A : CommRingCat} [TopologicalSpace ↑R] [IsTopologicalRing ↑R] [T1Space ↑R] [CompactSpace ↑R] :
              CompactSpace (A ⟶ R)
              source
              theorem CommRingCat.HomTopology.isEmbedding_pushout {R A B C : CommRingCat} [TopologicalSpace ↑R] [IsTopologicalRing ↑R] (φ : A ⟶ B) (ψ : A ⟶ C) :
              Topology.IsEmbedding fun (f : CategoryTheory.Limits.pushout φ ψ ⟶ R) => (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl φ ψ) f, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr φ ψ) f)

              Hom(B ⊗[A] C, R) has the subspace topology from Hom(B, R) × Hom(C, R).