Topological simplices #

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

We define the natural functor from simplex_category to Top sending [n] to the topological n-simplex. This is used to define Top.to_sSet in algebraic_topology.simpliciaL_set.

source

def simplex_category.to_Top_obj (x : simplex_category) :

set (↥x → nnreal)

The topological simplex associated to x : simplex_category. This is the object part of the functor simplex_category.to_Top.

Equations

x.to_Top_obj = {f : ↥x → nnreal | finset.univ.sum (λ (i : ↥x), f i) = 1}

Instances for ↥simplex_category.to_Top_obj

simplex_category.to_Top_obj.has_coe_to_fun

source

@[protected, instance]

def simplex_category.to_Top_obj.has_coe_to_fun (x : simplex_category) :

has_coe_to_fun ↥(x.to_Top_obj) (λ (_x : ↥(x.to_Top_obj)), ↥x → nnreal)

Equations

simplex_category.to_Top_obj.has_coe_to_fun x = {coe := λ (f : ↥(x.to_Top_obj)), ↑f}

source

@[ext]

theorem simplex_category.to_Top_obj.ext {x : simplex_category} (f g : ↥(x.to_Top_obj)) :

⇑f = ⇑g → f = g

source

def simplex_category.to_Top_map {x y : simplex_category} (f : x ⟶ y) :

↥(x.to_Top_obj) → ↥(y.to_Top_obj)

A morphism in simplex_category induces a map on the associated topological spaces.

Equations

simplex_category.to_Top_map f = λ (g : ↥(x.to_Top_obj)), ⟨λ (i : ↥y), (finset.filter (λ (k : ↥x), ⇑f k = i) finset.univ).sum (λ (j : ↥x), ⇑g j), _⟩

source

@[simp]

theorem simplex_category.coe_to_Top_map {x y : simplex_category} (f : x ⟶ y) (g : ↥(x.to_Top_obj)) (i : ↥y) :

⇑(simplex_category.to_Top_map f g) i = (finset.filter (λ (k : ↥x), ⇑f k = i) finset.univ).sum (λ (j : ↥x), ⇑g j)

source

@[continuity]

theorem simplex_category.continuous_to_Top_map {x y : simplex_category} (f : x ⟶ y) :

continuous (simplex_category.to_Top_map f)

source

def simplex_category.to_Top :

simplex_category ⥤ Top

The functor associating the topological n-simplex to [n] : simplex_category.

Equations

simplex_category.to_Top = {obj := λ (x : simplex_category), Top.of ↥(x.to_Top_obj), map := λ (x y : simplex_category) (f : x ⟶ y), {to_fun := simplex_category.to_Top_map f, continuous_to_fun := _}, map_id' := simplex_category.to_Top._proof_1, map_comp' := simplex_category.to_Top._proof_2}

source

@[simp]

theorem simplex_category.to_Top_map_apply (x y : simplex_category) (f : x ⟶ y) (ᾰ : ↥(x.to_Top_obj)) :

⇑(simplex_category.to_Top.map f) ᾰ = simplex_category.to_Top_map f ᾰ

source

@[simp]

theorem simplex_category.to_Top_obj_2 (x : simplex_category) :

simplex_category.to_Top.obj x = Top.of ↥(x.to_Top_obj)