Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
refactor(category_theory/concrete_category): move
bundled
to own file
- Loading branch information
Showing
8 changed files
with
99 additions
and
69 deletions.
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,95 @@ | ||
/- | ||
Copyright (c) 2018 Scott Morrison. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Scott Morrison, Johannes Hölzl, Reid Barton, Sean Leather | ||
Bundled type and structure. | ||
-/ | ||
import category_theory.functor | ||
import category_theory.types | ||
|
||
universes u v | ||
|
||
namespace category_theory | ||
variables {c d : Type u → Type v} {α : Type u} | ||
|
||
/-- | ||
`concrete_category @hom` collects the evidence that a type constructor `c` and a | ||
morphism predicate `hom` can be thought of as a concrete category. | ||
In a typical example, `c` is the type class `topological_space` and `hom` is | ||
`continuous`. | ||
-/ | ||
structure concrete_category (hom : out_param $ ∀ {α β}, c α → c β → (α → β) → Prop) := | ||
(hom_id : ∀ {α} (ia : c α), hom ia ia id) | ||
(hom_comp : ∀ {α β γ} (ia : c α) (ib : c β) (ic : c γ) {f g}, hom ia ib f → hom ib ic g → hom ia ic (g ∘ f)) | ||
|
||
attribute [class] concrete_category | ||
|
||
/-- `bundled` is a type bundled with a type class instance for that type. Only | ||
the type class is exposed as a parameter. -/ | ||
structure bundled (c : Type u → Type v) : Type (max (u+1) v) := | ||
(α : Type u) | ||
(str : c α) | ||
|
||
def mk_ob {c : Type u → Type v} (α : Type u) [str : c α] : bundled c := ⟨α, str⟩ | ||
|
||
namespace bundled | ||
|
||
instance : has_coe_to_sort (bundled c) := | ||
{ S := Type u, coe := bundled.α } | ||
|
||
/-- Map over the bundled structure -/ | ||
def map (f : ∀ {α}, c α → d α) (b : bundled c) : bundled d := | ||
⟨b.α, f b.str⟩ | ||
|
||
section concrete_category | ||
variables (hom : ∀ {α β : Type u}, c α → c β → (α → β) → Prop) | ||
variables [h : concrete_category @hom] | ||
include h | ||
|
||
instance : category (bundled c) := | ||
{ hom := λ a b, subtype (hom a.2 b.2), | ||
id := λ a, ⟨@id a.1, h.hom_id a.2⟩, | ||
comp := λ a b c f g, ⟨g.1 ∘ f.1, h.hom_comp a.2 b.2 c.2 f.2 g.2⟩ } | ||
|
||
variables {X Y Z : bundled c} | ||
|
||
@[simp] lemma concrete_category_id (X : bundled c) : subtype.val (𝟙 X) = id := | ||
rfl | ||
|
||
@[simp] lemma concrete_category_comp (f : X ⟶ Y) (g : Y ⟶ Z) : | ||
subtype.val (f ≫ g) = g.val ∘ f.val := | ||
rfl | ||
|
||
instance : has_coe_to_fun (X ⟶ Y) := | ||
{ F := λ f, X → Y, | ||
coe := λ f, f.1 } | ||
|
||
@[simp] lemma bundled_hom_coe {X Y : bundled c} (val : X → Y) (prop) (x : X) : | ||
(⟨val, prop⟩ : X ⟶ Y) x = val x := rfl | ||
|
||
end concrete_category | ||
|
||
end bundled | ||
|
||
def concrete_functor | ||
{C : Type u → Type v} {hC : ∀{α β}, C α → C β → (α → β) → Prop} [concrete_category @hC] | ||
{D : Type u → Type v} {hD : ∀{α β}, D α → D β → (α → β) → Prop} [concrete_category @hD] | ||
(m : ∀{α}, C α → D α) (h : ∀{α β} {ia : C α} {ib : C β} {f}, hC ia ib f → hD (m ia) (m ib) f) : | ||
bundled C ⥤ bundled D := | ||
{ obj := bundled.map @m, | ||
map := λ X Y f, ⟨ f, h f.2 ⟩} | ||
|
||
section forget | ||
variables {C : Type u → Type v} {hom : ∀α β, C α → C β → (α → β) → Prop} [i : concrete_category hom] | ||
include i | ||
|
||
/-- The forgetful functor from a bundled category to `Type`. -/ | ||
def forget : bundled C ⥤ Type u := { obj := bundled.α, map := λa b h, h.1 } | ||
|
||
instance forget.faithful : faithful (forget : bundled C ⥤ Type u) := {} | ||
|
||
end forget | ||
|
||
end category_theory |
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
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