Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit d91428c

Browse files
kim-emjohoelzl
authored andcommitted
feat(category_theory): the category of topological spaces, and of neighbourhoods of a point. also the category of commutative rings
1 parent e95111d commit d91428c

File tree

3 files changed

+118
-0
lines changed

3 files changed

+118
-0
lines changed

analysis/topology/topological_structures.lean

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -254,6 +254,10 @@ instance topological_ring.to_topological_semiring
254254
instance topological_ring.to_topological_add_group
255255
[topological_space α] [ring α] [t : topological_ring α] : topological_add_group α := {..t}
256256

257+
/-- A topological commutative ring is a commutative ring where the ring operations are continuous. -/
258+
class topological_comm_ring (α : Type u) [topological_space α] [comm_ring α]
259+
extends topological_ring α : Prop.
260+
257261
/-- (Partially) ordered topology
258262
Also called: partially ordered spaces (pospaces).
259263

category_theory/examples/rings.lean

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
-- Copyright (c) 2018 Scott Morrison. All rights reserved.
2+
-- Released under Apache 2.0 license as described in the file LICENSE.
3+
-- Authors: Scott Morrison
4+
5+
import category_theory.functor
6+
import algebra.ring
7+
import analysis.topology.topological_structures
8+
9+
open category_theory
10+
11+
namespace category_theory.examples
12+
13+
universe u₁
14+
15+
def CommRing : Type (u₁+1) := Σ α : Type u₁, comm_ring α
16+
17+
instance comm_ring_from_CommRing (R : CommRing) : comm_ring R.1 := R.2
18+
19+
structure comm_ring_hom (R S : CommRing.{u₁}) : Type u₁ :=
20+
(map: R.1 → S.1)
21+
(is_ring_hom : is_ring_hom map . obviously)
22+
23+
instance (R S : CommRing.{u₁}) (f : comm_ring_hom R S) : is_ring_hom f.map := f.is_ring_hom
24+
25+
@[simp] lemma comm_ring_hom.map_mul (R S : CommRing.{u₁}) (f : comm_ring_hom R S) (x y : R.1) :
26+
f.map(x * y) = (f.map x) * (f.map y) :=
27+
by rw f.is_ring_hom.map_mul
28+
@[simp] lemma comm_ring_hom.map_add (R S : CommRing.{u₁}) (f : comm_ring_hom R S) (x y : R.1) :
29+
f.map(x + y) = (f.map x) + (f.map y) :=
30+
by rw f.is_ring_hom.map_add
31+
@[simp] lemma comm_ring_hom.map_one (R S : CommRing.{u₁}) (f : comm_ring_hom R S) : f.map 1 = 1 :=
32+
by rw f.is_ring_hom.map_one
33+
34+
def comm_ring_hom.id (R : CommRing) : comm_ring_hom R R :=
35+
{ map := id }
36+
37+
@[simp] lemma comm_ring_hom.id_map (R : CommRing) (r : R.1) : (comm_ring_hom.id R).map r = r := rfl
38+
39+
def comm_ring_hom.comp {R S T : CommRing} (f: comm_ring_hom R S) (g : comm_ring_hom S T) : comm_ring_hom R T :=
40+
{ map := λ x, g.map (f.map x) }
41+
42+
@[simp] lemma comm_ring_hom.comp_map {R S T: CommRing} (f : comm_ring_hom R S) (g : comm_ring_hom S T) (r : R.1) :
43+
(comm_ring_hom.comp f g).map r = g.map (f.map r) := rfl
44+
45+
@[extensionality] lemma comm_ring_hom.ext {R S : CommRing} (f g : comm_ring_hom R S) (w : ∀ x : R.1, f.map x = g.map x) : f = g :=
46+
begin
47+
induction f with fc,
48+
induction g with gc,
49+
tidy,
50+
end
51+
52+
instance : large_category CommRing :=
53+
{ hom := comm_ring_hom,
54+
id := comm_ring_hom.id,
55+
comp := @comm_ring_hom.comp }
56+
57+
end category_theory.examples
Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
-- Copyright (c) 2017 Scott Morrison. All rights reserved.
2+
-- Released under Apache 2.0 license as described in the file LICENSE.
3+
-- Authors: Patrick Massot, Scott Morrison
4+
5+
import category_theory.full_subcategory
6+
import analysis.topology.topological_space
7+
import analysis.topology.continuity
8+
9+
open category_theory
10+
11+
namespace category_theory.examples.topological_spaces
12+
13+
universe u₁
14+
15+
def Top : Type (u₁+1) := Σ α : Type u₁, topological_space α
16+
17+
instance (X : Top) : topological_space X.1 := X.2
18+
19+
structure continuous_map (X Y : Top.{u₁}) : Type u₁ :=
20+
(map : X.1 → Y.1 )
21+
(continuous : continuous map)
22+
23+
@[extensionality] lemma continuous_map.ext
24+
{X Y : Top.{u₁}} (f g : continuous_map X Y) (w : ∀ x : X.1, f.map x = g.map x) : f = g :=
25+
begin
26+
induction f with fc,
27+
induction g with gc,
28+
tidy,
29+
end
30+
31+
instance : large_category Top :=
32+
{ hom := continuous_map,
33+
id := λ X, ⟨ id, continuous_id ⟩,
34+
comp := λ _ _ _ f g, ⟨ g.map ∘ f.map, continuous.comp f.continuous g.continuous ⟩ }
35+
36+
structure open_set (α : Type u₁) [X : topological_space α] : Type u₁ :=
37+
(s : set α)
38+
(is_open : topological_space.is_open X s)
39+
40+
variables {α : Type u₁} [topological_space α]
41+
42+
instance : has_coe (open_set α) (set α) := { coe := λ U, U.s }
43+
44+
instance : has_subset (open_set α) :=
45+
{ subset := λ U V, U.s ⊆ V.s }
46+
47+
instance : preorder (open_set α) := by refine { le := (⊆), .. } ; tidy
48+
49+
instance open_sets : small_category (open_set α) := by apply_instance
50+
51+
instance : has_mem α (open_set α) :=
52+
{ mem := λ a V, a ∈ V.s }
53+
54+
def nbhd (x : α) := { U : open_set α // x ∈ U }
55+
def nbhds (x : α) : small_category (nbhd x) := begin unfold nbhd, apply_instance end
56+
57+
end category_theory.examples.topological_spaces

0 commit comments

Comments
 (0)