Presheaves of functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We construct some simple examples of presheaves of functions on a topological space.
presheaf_to_Types X T, whereT : X → Type, is the presheaf of dependently-typed (not-necessarily continuous) functionspresheaf_to_Type X T, whereT : Type, is the presheaf of (not-necessarily-continuous) functions to a fixed target typeTpresheaf_to_Top X T, whereT : Top, is the presheaf of continuous functions into a topological spaceTpresheaf_To_TopCommRing X R, whereR : TopCommRingis the presheaf valued inCommRingof functions functions into a topological ringR- as an example of the previous construction,
presheaf_to_TopCommRing X (TopCommRing.of ℂ)is the presheaf of rings of continuous complex-valued functions onX.
The presheaf of dependently typed functions on X, with fibres given by a type family T.
There is no requirement that the functions are continuous, here.
Equations
- X.presheaf_to_Types T = {obj := λ (U : (topological_space.opens ↥X)ᵒᵖ), Π (x : ↥(opposite.unop U)), T ↑x, map := λ (U V : (topological_space.opens ↥X)ᵒᵖ) (i : U ⟶ V) (g : Π (x : ↥(opposite.unop U)), T ↑x) (x : ↥(opposite.unop V)), g (⇑(i.unop) x), map_id' := _, map_comp' := _}
The presheaf of functions on X with values in a type T.
There is no requirement that the functions are continuous, here.
Equations
- X.presheaf_to_Type T = {obj := λ (U : (topological_space.opens ↥X)ᵒᵖ), ↥(opposite.unop U) → T, map := λ (U V : (topological_space.opens ↥X)ᵒᵖ) (i : U ⟶ V) (g : ↥(opposite.unop U) → T), g ∘ ⇑(i.unop), map_id' := _, map_comp' := _}
The presheaf of continuous functions on X with values in fixed target topological space
T.
Equations
The (bundled) commutative ring of continuous functions from a topological space to a topological commutative ring, with pointwise multiplication.
Equations
Pulling back functions into a topological ring along a continuous map is a ring homomorphism.
A homomorphism of topological rings can be postcomposed with functions from a source space X;
this is a ring homomorphism (with respect to the pointwise ring operations on functions).
Equations
- Top.continuous_functions.map X φ = {to_fun := λ (g : ↥(Top.continuous_functions X R)), g ≫ (category_theory.forget₂ TopCommRing Top).map φ, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
An upgraded version of the Yoneda embedding, observing that the continuous maps
from X : Top to R : TopCommRing form a commutative ring, functorial in both X and R.
Equations
- Top.CommRing_yoneda = {obj := λ (R : TopCommRing), {obj := λ (X : Topᵒᵖ), Top.continuous_functions X R, map := λ (X Y : Topᵒᵖ) (f : X ⟶ Y), Top.continuous_functions.pullback f R, map_id' := _, map_comp' := _}, map := λ (R S : TopCommRing) (φ : R ⟶ S), {app := λ (X : Topᵒᵖ), Top.continuous_functions.map X φ, naturality' := _}, map_id' := Top.CommRing_yoneda._proof_8, map_comp' := Top.CommRing_yoneda._proof_9}
The presheaf (of commutative rings), consisting of functions on an open set U ⊆ X with
values in some topological commutative ring T.
For example, we could construct the presheaf of continuous complex valued functions of X as
presheaf_to_TopCommRing X (TopCommRing.of ℂ)
(this requires import topology.instances.complex).