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

• CommRingCat.HomTopology.isClosedEmbedding_precomp_of_surjective: Hom(A/I, R) is a closed subspace of Hom(A, R) if R is Hausdorff.
• CommRingCat.HomTopology.mvPolynomialHomeo: Hom(A[Xᵢ], R) is homeomorphic to Hom(A, R) × Rᶥ.
• CommRingCat.HomTopology.isEmbedding_pushout: Hom(B ⊗[A] C, R) has the subspace topology from Hom(B, R) × Hom(C, R).

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 mvPolynomialHomeo).

This is a scoped instance in CommRingCat.HomTopology.

Equations

• CommRingCat.HomTopology.instTopologicalSpaceHom = TopologicalSpace.induced (fun (f : A ⟶ R) => ⇑(CommRingCat.Hom.hom f)) inferInstance

theorem CommRingCat.HomTopology.continuous_apply {R A : CommRingCat} [TopologicalSpace ↑R] (x : ↑A) : Continuous fun (f : A ⟶ R) => (Hom.hom f) x

theorem CommRingCat.HomTopology.isEmbedding_hom (R A : CommRingCat) [TopologicalSpace ↑R] : Topology.IsEmbedding fun (f : A ⟶ R) => ⇑(Hom.hom f)

theorem CommRingCat.HomTopology.continuous_precomp {R A B : CommRingCat} [TopologicalSpace ↑R] (f : A ⟶ B) : Continuous fun (x : B ⟶ R) => CategoryTheory.CategoryStruct.comp f x

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 homeomorphc to Hom(B, R).

Equations

• One or more equations did not get rendered due to their size.

@[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 φ

@[simp]

theorem CommRingCat.HomTopology.precompHomeomorph_apply {R A B : CommRingCat} [TopologicalSpace ↑R] (f : A ≅ B) (φ : B ⟶ R) : (precompHomeomorph f) φ = CategoryTheory.CategoryStruct.comp f.hom φ

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

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)

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.

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

• One or more equations did not get rendered due to their size.

@[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

@[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)

@[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

theorem CommRingCat.HomTopology.isClosedEmbedding_hom (R A : CommRingCat) [TopologicalSpace ↑R] [IsTopologicalRing ↑R] [T1Space ↑R] : Topology.IsClosedEmbedding fun (f : A ⟶ R) => ⇑(Hom.hom f)

instance CommRingCat.HomTopology.instT2SpaceHomOfCarrier {R A : CommRingCat} [TopologicalSpace ↑R] [T2Space ↑R] : T2Space (A ⟶ R)

instance CommRingCat.HomTopology.instCompactSpaceHomOfIsTopologicalRingOfT1SpaceOfCarrier {R A : CommRingCat} [TopologicalSpace ↑R] [IsTopologicalRing ↑R] [T1Space ↑R] [CompactSpace ↑R] : CompactSpace (A ⟶ R)

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).