Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(Top.presheaf_ℂ): presheaves of functions to topological commutat…
…ive rings (#976) * feat(category_theory/colimits): missing simp lemmas * feat(category_theory): functor.map_nat_iso * define `functor.map_nat_iso`, and relate to whiskering * rename `functor.on_iso` to `functor.map_iso` * add some missing lemmas about whiskering * fix(category_theory): presheaves, unbundled and bundled, and pushforwards * restoring `(opens X)ᵒᵖ` * various changes from working on stalks * rename `nbhds` to `open_nhds` * fix introduced typo * typo * compactify a proof * rename `presheaf` to `presheaf_on_space` * fix(category_theory): turn `has_limits` classes into structures * naming instances to avoid collisions * breaking up instances.topological_spaces * fixing all the other pi-type typclasses * fix import * oops * fix import * missed one * typo * WIP * oops * the presheaf of continuous functions to ℂ * restoring eq_to_hom simp lemmas * removing unnecessary simp lemma * remove another superfluous lemma * removing the nat_trans and vcomp notations; use \hom and \gg * a simpler proposal * getting rid of vcomp * fix * splitting files * renaming * update notation * fix * cleanup * use iso_whisker_right instead of map_nat_iso * proofs magically got easier? * improve some proofs * moving instances * remove crap * tidy * minimise imports * chore(travis): disable the check for minimal imports * Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: semorrison <scott@tqft.net> * writing `op_induction` tactic, and improving proofs * squeeze_simping * cleanup * rearranging * cleanup * cleaning up * cleaning up * move * Update src/category_theory/instances/Top/presheaf_of_functions.lean Co-Authored-By: Floris van Doorn <fpvdoorn@gmail.com> * fixes in response to review
- Loading branch information
1 parent
b9b5bb4
commit 70cd00b
Showing
6 changed files
with
166 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
74 changes: 74 additions & 0 deletions
74
src/category_theory/instances/Top/presheaf_of_functions.lean
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,74 @@ | ||
import category_theory.instances.Top.presheaf | ||
import category_theory.instances.TopCommRing.basic | ||
import category_theory.yoneda | ||
import ring_theory.subring | ||
import topology.algebra.continuous_functions | ||
|
||
universes v u | ||
|
||
open category_theory | ||
open category_theory.instances | ||
open topological_space | ||
|
||
namespace category_theory.instances.Top | ||
|
||
variables (X : Top.{v}) | ||
|
||
def presheaf_to_Top (T : Top.{v}) : X.presheaf (Type v) := | ||
(opens.to_Top X).op ⋙ (yoneda.obj T) | ||
|
||
-- TODO upgrade the result to TopCommRing? | ||
def continuous_functions (X : Top.{v}ᵒᵖ) (R : TopCommRing.{v}) : CommRing.{v} := | ||
{ α := unop X ⟶ TopCommRing.forget_to_Top.obj R, | ||
str := _root_.continuous_comm_ring } | ||
|
||
namespace continuous_functions | ||
@[simp] lemma one (X : Top.{v}ᵒᵖ) (R : TopCommRing.{v}) (x) : | ||
(monoid.one ↥(continuous_functions X R)).val x = 1 := rfl | ||
@[simp] lemma add (X : Top.{v}ᵒᵖ) (R : TopCommRing.{v}) (f g : continuous_functions X R) (x) : | ||
(comm_ring.add f g).val x = f.1 x + g.1 x := rfl | ||
@[simp] lemma mul (X : Top.{v}ᵒᵖ) (R : TopCommRing.{v}) (f g : continuous_functions X R) (x) : | ||
(ring.mul f g).val x = f.1 x * g.1 x := rfl | ||
|
||
def pullback {X Y : Topᵒᵖ} (f : X ⟶ Y) (R : TopCommRing) : | ||
continuous_functions X R ⟶ continuous_functions Y R := | ||
{ val := λ g, f.unop ≫ g, | ||
property := | ||
{ map_one := rfl, | ||
map_add := by tidy, | ||
map_mul := by tidy } } | ||
|
||
local attribute [extensionality] subtype.eq | ||
|
||
def map (X : Topᵒᵖ) {R S : TopCommRing} (φ : R ⟶ S) : | ||
continuous_functions X R ⟶ continuous_functions X S := | ||
{ val := λ g, g ≫ (TopCommRing.forget_to_Top.map φ), | ||
property := | ||
{ map_one := begin ext1, ext1, simp only [one], exact φ.2.1.map_one end, | ||
map_add := λ x y, | ||
begin ext1, ext1, simp only [function.comp_app, add], apply φ.2.1.map_add end, | ||
map_mul := λ x y, | ||
begin ext1, ext1, simp only [function.comp_app, mul], apply φ.2.1.map_mul end } } | ||
end continuous_functions | ||
|
||
def CommRing_yoneda : TopCommRing ⥤ (Topᵒᵖ ⥤ CommRing) := | ||
{ obj := λ R, | ||
{ obj := λ X, continuous_functions X R, | ||
map := λ X Y f, continuous_functions.pullback f R }, | ||
map := λ R S φ, | ||
{ app := λ X, continuous_functions.map X φ } } | ||
|
||
def presheaf_to_TopCommRing (T : TopCommRing.{v}) : | ||
X.presheaf CommRing.{v} := | ||
(opens.to_Top X).op ⋙ (CommRing_yoneda.obj T) | ||
|
||
noncomputable def presheaf_ℚ (Y : Top) : Y.presheaf CommRing := | ||
presheaf_to_TopCommRing Y (TopCommRing.of ℚ) | ||
|
||
noncomputable def presheaf_ℝ (Y : Top) : Y.presheaf CommRing := | ||
presheaf_to_TopCommRing Y (TopCommRing.of ℝ) | ||
|
||
noncomputable def presheaf_ℂ (Y : Top) : Y.presheaf CommRing := | ||
presheaf_to_TopCommRing Y (TopCommRing.of ℂ) | ||
|
||
end category_theory.instances.Top |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,83 @@ | ||
import category_theory.instances.CommRing.basic | ||
import category_theory.instances.Top.basic | ||
import topology.instances.complex | ||
|
||
universes u | ||
|
||
open category_theory | ||
|
||
namespace category_theory.instances | ||
|
||
structure TopCommRing := | ||
(α : Type u) | ||
[is_comm_ring : comm_ring α] | ||
[is_topological_space : topological_space α] | ||
[is_topological_ring : topological_ring α] | ||
|
||
instance : has_coe_to_sort TopCommRing := | ||
{ S := Type u, coe := TopCommRing.α } | ||
|
||
instance TopCommRing_comm_ring (R : TopCommRing) : comm_ring R := R.is_comm_ring | ||
instance TopCommRing_topological_space (R : TopCommRing) : topological_space R := R.is_topological_space | ||
instance TopCommRing_topological_ring (R : TopCommRing) : topological_ring R := R.is_topological_ring | ||
|
||
instance TopCommRing_category : category TopCommRing := | ||
{ hom := λ R S, {f : R → S // is_ring_hom f ∧ continuous f }, | ||
id := λ R, ⟨id, by obviously⟩, | ||
comp := λ R S T f g, ⟨g.val ∘ f.val, | ||
begin -- TODO automate | ||
cases f, cases g, cases f_property, cases g_property, split, | ||
dsimp, resetI, apply_instance, | ||
dsimp, apply continuous.comp ; assumption | ||
end⟩ }. | ||
|
||
namespace TopCommRing | ||
|
||
def of (X : Type u) [comm_ring X] [topological_space X] [topological_ring X] : TopCommRing := | ||
{ α := X } | ||
|
||
noncomputable example : TopCommRing := TopCommRing.of ℚ | ||
noncomputable example : TopCommRing := TopCommRing.of ℝ | ||
noncomputable example : TopCommRing := TopCommRing.of ℂ | ||
|
||
/-- The forgetful functor to CommRing. -/ | ||
def forget_to_CommRing : TopCommRing ⥤ CommRing := | ||
{ obj := λ R, { α := R, str := instances.TopCommRing_comm_ring R }, | ||
map := λ R S f, ⟨ f.1, f.2.left ⟩ } | ||
|
||
instance forget_to_CommRing_faithful : faithful (forget_to_CommRing) := by tidy | ||
|
||
instance forget_to_CommRing_topological_space (R : TopCommRing) : topological_space (forget_to_CommRing.obj R) := | ||
R.is_topological_space | ||
|
||
/-- The forgetful functor to Top. -/ | ||
def forget_to_Top : TopCommRing ⥤ Top := | ||
{ obj := λ R, { α := R, str := instances.TopCommRing_topological_space R }, | ||
map := λ R S f, ⟨ f.1, f.2.right ⟩ } | ||
|
||
instance forget_to_Top_faithful : faithful (forget_to_Top) := by tidy | ||
|
||
instance forget_to_Top_comm_ring (R : TopCommRing) : comm_ring (forget_to_Top.obj R) := | ||
R.is_comm_ring | ||
instance forget_to_Top_topological_ring (R : TopCommRing) : topological_ring (forget_to_Top.obj R) := | ||
R.is_topological_ring | ||
|
||
def forget : TopCommRing ⥤ (Type u) := | ||
{ obj := λ R, R, | ||
map := λ R S f, f.1 } | ||
|
||
instance forget_faithful : faithful (forget) := by tidy | ||
|
||
instance forget_topological_space (R : TopCommRing) : topological_space (forget.obj R) := | ||
R.is_topological_space | ||
instance forget_comm_ring (R : TopCommRing) : comm_ring (forget.obj R) := | ||
R.is_comm_ring | ||
instance forget_topological_ring (R : TopCommRing) : topological_ring (forget.obj R) := | ||
R.is_topological_ring | ||
|
||
def forget_to_Type_via_Top : forget_to_Top ⋙ category_theory.forget ≅ forget := iso.refl _ | ||
def forget_to_Type_via_CommRing : forget_to_Top ⋙ category_theory.forget ≅ forget := iso.refl _ | ||
|
||
end TopCommRing | ||
|
||
end category_theory.instances |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
import category_theory.instances.TopCommRing.basic |