mathlib docs: topology.category.TopCommRing

source

structure TopCommRing :

Type (u+1)

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

A bundled topological commutative ring.

source

@[instance]

def TopCommRing.has_coe_to_sort :

has_coe_to_sort TopCommRing

Equations

TopCommRing.has_coe_to_sort = {S := Type u, coe := TopCommRing.α}

source

@[instance]

def TopCommRing.category_theory.category :

category_theory.category TopCommRing

Equations

TopCommRing.category_theory.category = {to_category_struct := {to_has_hom := {hom := λ (R S : TopCommRing), {f // continuous ⇑f}}, id := λ (R : TopCommRing), ⟨ring_hom.id ↥R ring.to_semiring, _⟩, 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

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

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

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

@[instance]

def TopCommRing.forget_topological_ring (R : TopCommRing) :

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

Equations

_ = _

source

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

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

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

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

@[instance]

def TopCommRing.forget_to_Top_topological_ring (R : TopCommRing) :

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

Equations

_ = _

source

@[instance]

def TopCommRing.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.

Equations

TopCommRing.category_theory.reflects_isomorphisms = {reflects := λ (X Y : TopCommRing) (f : X ⟶ Y) (_x : category_theory.is_iso ((category_theory.forget₂ TopCommRing Top).map f)), let i_Top : (category_theory.forget₂ TopCommRing Top).obj X ≅ (category_theory.forget₂ TopCommRing Top).obj Y := category_theory.as_iso ((category_theory.forget₂ TopCommRing Top).map f), e_Ring : ↥X ≃+* ↥Y := {to_fun := f.val.to_fun, inv_fun := ((category_theory.forget Top).map_iso i_Top).to_equiv.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _} in {inv := ⟨↑(e_Ring.symm), _⟩, hom_inv_id' := _, inv_hom_id' := _}}

mathlib documentation

topology.category.TopCommRing

General documentation

Additional documentation

Library

mathlib documentation

topology.​category.​TopCommRing

General documentation

Additional documentation

Library

topology.category.TopCommRing