Category of topological commutative rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We introduce the category TopCommRing of topological commutative rings together with the relevant forgetful functors to topological spaces and commutative rings.

source

structure TopCommRing :

Type (u+1)

α : Type ?
is_comm_ring : comm_ring self.α
is_topological_space : topological_space self.α
is_topological_ring : topological_ring self.α

A bundled topological commutative ring.

Instances for TopCommRing

TopCommRing.has_sizeof_inst
TopCommRing.inhabited
TopCommRing.has_coe_to_sort
TopCommRing.category_theory.category
TopCommRing.category_theory.concrete_category
TopCommRing.has_forget_to_CommRing
TopCommRing.has_forget_to_Top

source

@[protected, instance]

def TopCommRing.inhabited :

inhabited TopCommRing

Equations

TopCommRing.inhabited = {default := {α := punit, is_comm_ring := punit.comm_ring, is_topological_space := punit.topological_space, is_topological_ring := TopCommRing.inhabited._proof_1}}

source

@[protected, instance]

def TopCommRing.has_coe_to_sort :

has_coe_to_sort TopCommRing (Type u)

Equations

TopCommRing.has_coe_to_sort = {coe := TopCommRing.α}

source

@[protected, instance]

def TopCommRing.category_theory.category :

category_theory.category TopCommRing

Equations

TopCommRing.category_theory.category = {to_category_struct := {to_quiver := {hom := λ (R S : TopCommRing), {f // continuous ⇑f}}, id := λ (R : TopCommRing), ⟨ring_hom.id ↥R (non_assoc_ring.to_non_assoc_semiring ↥R), _⟩, comp := λ (R S T : TopCommRing) (f : R ⟶ S) (g : S ⟶ T), ⟨g.val.comp f.val, _⟩}, id_comp' := TopCommRing.category_theory.category._proof_3, comp_id' := TopCommRing.category_theory.category._proof_4, assoc' := TopCommRing.category_theory.category._proof_5}

source

@[protected, instance]

def TopCommRing.category_theory.concrete_category :

category_theory.concrete_category TopCommRing

Equations

TopCommRing.category_theory.concrete_category = category_theory.concrete_category.mk {obj := λ (R : TopCommRing), ↥R, map := λ (R S : TopCommRing) (f : R ⟶ S), ⇑(f.val), map_id' := TopCommRing.category_theory.concrete_category._proof_1, map_comp' := TopCommRing.category_theory.concrete_category._proof_2}

source

def TopCommRing.of (X : Type u) [comm_ring X] [topological_space X] [topological_ring X] :

TopCommRing

Construct a bundled TopCommRing from the underlying type and the appropriate typeclasses.

Equations

TopCommRing.of X = TopCommRing.mk X

source

@[simp]

theorem TopCommRing.coe_of (X : Type u) [comm_ring X] [topological_space X] [topological_ring X] :

↥(TopCommRing.of X) = X

source

@[protected, instance]

def TopCommRing.forget_topological_space (R : TopCommRing) :

topological_space ((category_theory.forget TopCommRing).obj R)

Equations

R.forget_topological_space = R.is_topological_space

source

@[protected, instance]

def TopCommRing.forget_comm_ring (R : TopCommRing) :

comm_ring ((category_theory.forget TopCommRing).obj R)

Equations

R.forget_comm_ring = R.is_comm_ring

source

@[protected, instance]

def TopCommRing.forget_topological_ring (R : TopCommRing) :

topological_ring ((category_theory.forget TopCommRing).obj R)

source

@[protected, instance]

def TopCommRing.has_forget_to_CommRing :

category_theory.has_forget₂ TopCommRing CommRing

Equations

TopCommRing.has_forget_to_CommRing = category_theory.has_forget₂.mk' (λ (R : TopCommRing), CommRing.of ↥R) TopCommRing.has_forget_to_CommRing._proof_1 (λ (R S : TopCommRing) (f : R ⟶ S), f.val) TopCommRing.has_forget_to_CommRing._proof_2

source

@[protected, instance]

def TopCommRing.forget_to_CommRing_topological_space (R : TopCommRing) :

topological_space ↥((category_theory.forget₂ TopCommRing CommRing).obj R)

Equations

R.forget_to_CommRing_topological_space = R.is_topological_space

source

@[protected, instance]

def TopCommRing.has_forget_to_Top :

category_theory.has_forget₂ TopCommRing Top

The forgetful functor to Top.

Equations

TopCommRing.has_forget_to_Top = category_theory.has_forget₂.mk' (λ (R : TopCommRing), Top.of ↥R) TopCommRing.has_forget_to_Top._proof_1 (λ (R S : TopCommRing) (f : R ⟶ S), {to_fun := ⇑(f.val), continuous_to_fun := _}) TopCommRing.has_forget_to_Top._proof_3

source

@[protected, instance]

def TopCommRing.forget_to_Top_comm_ring (R : TopCommRing) :

comm_ring ↥((category_theory.forget₂ TopCommRing Top).obj R)

Equations

R.forget_to_Top_comm_ring = R.is_comm_ring

source

@[protected, instance]

def TopCommRing.forget_to_Top_topological_ring (R : TopCommRing) :

topological_ring ↥((category_theory.forget₂ TopCommRing Top).obj R)

source

@[protected, instance]

def TopCommRing.category_theory.forget₂.category_theory.reflects_isomorphisms :

category_theory.reflects_isomorphisms (category_theory.forget₂ TopCommRing Top)

The forgetful functors to Type do not reflect isomorphisms, but the forgetful functor from TopCommRing to Top does.