Clean up cat theory notes

Changes

2 changed files (+240/-74)

• Category.lean (new)
  • @@ -0,0 +1,240 @@
    + import Mathlib + + /- + Lean, the category! + Objects: Types + Morphisms: (Total) Functions + + Resources: + https://raw.githubusercontent.com/BartoszMilewski/DaoFP/refs/heads/master/DaoFP.pdf + https://math.andrej.com/2016/08/06/hask-is-not-a-category/ + -/ + + -- Initial object + #check Empty + + -- Morphism from initial object + #check Empty.elim + + -- Terminal object + #check PUnit + + -- Identity morphism + #check id + + -- Composition of morphism is associative + #check Function.comp_assoc + + -- Equality of morphisms + #check funext + + -- Sums (coproducts) + #check Sum + + -- Products + #check Prod + + -- Exponentials + #check (· → ·) + + + /- + Endofunctors + f maps objects + f.map maps morphisms + `(α → β) → f α → f β` is the same thing as `(α → β) → (f α → f β)` + -/ + #check Functor + #check LawfulFunctor + + #synth Functor List + + #synth Functor Option + + instance : LawfulFunctor List where + map_const := by solve_by_elim + id_map xs := by simp + comp_map := by simp + + + /-- + Contravariant (endo)functors (normal functors are "covariant" functors) + + Also, contravariant functors are covariant functors in the opposite category + + `map` turns a "producer of α" into a "producer of β" + `comap` turns a "consumer of α" into a "consumer of β" + -/ + class Cofunctor (f : Type u → Type v) where + comap : (β → α) → f α → f β + id_comap (x : f α) : comap id x = x + comp_comap (g : β → α) (h : γ → β) (x : f α) : comap (g ∘ h) x = comap h (comap g x) + + theorem Cofunctor.id_comap' [Cofunctor f] : Cofunctor.comap (f := f) (@id α) = id := by + ext x + exact Cofunctor.id_comap (f := f) x + + theorem Cofunctor.comap_comp_comap [Cofunctor f] (g : α → β) (h : β → γ) : + ((Cofunctor.comap g) ∘ (Cofunctor.comap h) : f γ → f α) = Cofunctor.comap (f := f) (h ∘ g) := + funext fun _ => (comp_comap _ _ _).symm + + + /-- Composition of two functors of same variance is a functor -/ + @[simp] + instance [Functor f] [LawfulFunctor f] [Functor g] [LawfulFunctor g] : Functor (f ∘ g) where + map h x := Functor.map (f := f) (h <$> ·) x + + instance [Functor f] [LawfulFunctor f] [Functor g] [LawfulFunctor g] : LawfulFunctor (f ∘ g) where + map_const := by solve_by_elim + id_map := by simp + comp_map h h' x := by simp; rfl + + @[simp] + instance [Cofunctor f] [Cofunctor g] : Functor (f ∘ g) where + map h x := Cofunctor.comap (f := f) (Cofunctor.comap h) x + + instance [Cofunctor f] [Cofunctor g] : LawfulFunctor (f ∘ g) where + map_const := by solve_by_elim + id_map := by simp [Cofunctor.id_comap'] + comp_map h h' x := by simp [← Cofunctor.comap_comp_comap] + + #synth LawfulFunctor (List ∘ Option) + + + /-- Composition of functors of opposite variance is a contravariant functor -/ + @[simp] + instance [Functor f] [LawfulFunctor f] [Cofunctor g] : Cofunctor (f ∘ g) where + comap h x := Functor.map (f := f) (Cofunctor.comap h ·) x + id_comap := by simp [Cofunctor.id_comap (f := g)] + comp_comap := by simp [Cofunctor.comp_comap] + + @[simp] + instance [Cofunctor f] [Functor g] [LawfulFunctor g] : Cofunctor (f ∘ g) where + comap h x := Cofunctor.comap (f := f) (h <$> ·) x + id_comap := by + simp only [Function.comp_apply, id_map] + exact Cofunctor.id_comap (f := f) + comp_comap h h' x := by + simp only [← Functor.map_comp_map h' h, Cofunctor.comp_comap (f := f)] + + + /-- Hom-functor in enriched category -/ + @[simp] + instance (α : Type u) : Functor (α → ·) where + map f g := f ∘ g + + instance (α : Type u) : LawfulFunctor (α → ·) where + map_const := by solve_by_elim + id_map := by simp + comp_map := by simp [Function.comp_assoc] + + @[simp] + instance (α : Type u) : Cofunctor (· → α) where + comap f g := g ∘ f + id_comap := by simp + comp_comap := by simp [Function.comp_assoc] + + + -- Bifunctors map Lean × Lean to Lean + #check Bifunctor + #check LawfulBifunctor + + + /-- Profunctors: Useful for lenses -/ + class Profunctor (p : Type u → Type u → Type (u + 1)) where + dimap : (s → a) → (b → t) → (p a b → p s t) + + inductive Procompose p q [Profunctor p] [Profunctor q] a b + | mk : q a x → p x b → Procompose p q a b + + def mapOut [Profunctor p] [Profunctor q] (pc : Procompose p q a b) (f : {x : Type} → q a x → p x b → c) := + match pc with + | ⟨qax, pxb⟩ => f qax pxb + + instance [Profunctor p] [Profunctor q] : Profunctor (Procompose p q) where + dimap l r + | ⟨qax, pxb⟩ => ⟨Profunctor.dimap l id qax, Profunctor.dimap id r pxb⟩ + + def End p [Profunctor p] := ∀ x, p x x + + def Coend p [Profunctor p] := Σ x, p x x + + inductive ProPair q p [Profunctor p] [Profunctor q] a b x y + | mk : q a y → p x b → ProPair q p a b x y + + instance [Profunctor p] [Profunctor q] : Profunctor (ProPair q p a b) where + dimap l r + | ⟨qax, pxb⟩ => ⟨Profunctor.dimap id r qax, Profunctor.dimap l id pxb⟩ + + inductive CoEndCompose p q [Profunctor p] [Profunctor q] a b + | mk : Coend (ProPair q p a b) → CoEndCompose p q a b + + instance [Profunctor p] [Profunctor q] : Profunctor (CoEndCompose p q) where + dimap l r + | ⟨x, ⟨qay, pxb⟩⟩ => ⟨x, ⟨Profunctor.dimap l id qay,Profunctor.dimap id r pxb⟩⟩ + + + /- Natural transformations -/ + class Natural f [Functor f] [LawfulFunctor f] g [Functor g] [LawfulFunctor g] (η : {α : Type u} → f α → g α) where + naturality (h : α → β) (x : f α) : h <$> (η x) = η (h <$> x) + + instance : Natural List Option List.head? where + naturality := by simp + + def OptionToList : Option α → List α + | some a => [a] + | none => [] + + instance : Natural Option List OptionToList where + naturality := by + simp [OptionToList] + grind + + class Conatural f [Cofunctor f] g [Cofunctor g] (η : {α : Type u} → f α → g α) where + naturality (h : β → α) (x : f α) : Cofunctor.comap h (η x) = η (Cofunctor.comap h x) + + + /-- + Yoneda forward map + g is not necessarily natural + -/ + def yoneda (g : {β : Type u} → (α → β) → f β) [Functor f] [LawfulFunctor f] : f α := g id + + /-- Yoneda reverse map -/ + def yoneda' [Functor f] [LawfulFunctor f] (y : f α) : {β : Type u} → (α → β) → f β := (· <$> y) + + /-- Reverse map always produces a natural transformation -/ + instance [Functor f] [LawfulFunctor f] : Natural (α → ·) f (yoneda' y) where + naturality h x := by simp [yoneda']; rfl + + /-- Mapping and unmapping a natural transformation returns the itself + Note that this does work for an arbitrary function between the hom-functor and `m` because we use the naturality condition. -/ + theorem yoneda_lemma (g : {β : Type u} → (α → β) → f β) [Functor f] [LawfulFunctor f] [N : Natural (α → ·) f g] + : (yoneda' (β := ·) (yoneda (f := f) g)) = (g (β := ·)) := by + unfold yoneda yoneda' + simp [N.naturality] + + /-- Mapping and unmapping an element `m α` returns itself -/ + theorem yoneda_lemma' (y : f α) [Functor f] [LawfulFunctor f] + : yoneda (yoneda' (f := f) (α := α) y) = y := by + simp [yoneda, yoneda'] + + + /-- Coyoneda forward map -/ + def coyoneda (g : {β : Type u} → (β → α) → f β) [Cofunctor f] : f α := g id + + /-- Coyoneda reverse map -/ + def coyoneda' [Cofunctor f] (y : f α) : {β : Type u} → (β → α) → f β := (Cofunctor.comap · y) + + /-- Same but for Coyoneda -/ + theorem coyoneda_lemma (g : {β : Type u} → (β → α) → f β) [Cofunctor f] [N : Conatural (· → α) f g] + : (coyoneda' (β := ·) (coyoneda (f := f) g)) = (g (β := ·)) := by + unfold coyoneda coyoneda' + simp [N.naturality] + + theorem coyoneda_lemma' (y : f α) [Cofunctor f] + : coyoneda (coyoneda' (f := f) (α := α) y) = y := by + simp [coyoneda, coyoneda', Cofunctor.id_comap] + + + -- TODO: Applicatives, monads, Kleisi categories
• Dao.lean
  • @@ -140,77 +140,3 @@ def getResidue : LensE s a → c
    | ⟨l, _⟩ => (l _).1 end Ch18 - - - namespace Yoneda - - class ContraFunctor (f : Type → Type) where - contramap : (β → α) → f α → f β - id_contramap (x : f α) : contramap id x = x - comp_contramap (g : β → α) (h : γ → β) (x : f α) : contramap (g ∘ h) x = contramap h (contramap g x) - - instance (α : Type) : ContraFunctor (· → α) where - contramap f g := fun x ↦ g (f x) - id_contramap := by simp - comp_contramap := by simp - - #synth Functor List - - #synth Functor Option - - instance : LawfulFunctor List where - map_const := by solve_by_elim - id_map xs := by simp - comp_map := by simp - - class Natural f [Functor f] [LawfulFunctor f] g [Functor g] [LawfulFunctor g] (η : {α : Type u} → f α → g α) where - naturality (x : f α) (h : α → β) : Functor.map h (η x) = η (Functor.map h x) - - instance : Natural List Option List.head? where - naturality x h := by simp - - def OptionToList : Option α → List α - | some a => [a] - | none => [] - - instance : Natural Option List OptionToList where - naturality x h := by - simp [OptionToList] - grind - - -- OK time to do Yoneda part 2 - - /-- Hom-functor in enriched category -/ - @[simp] - instance (α : Type u) : Functor (α → ·) where - map f g := f ∘ g - - instance (α : Type u) : LawfulFunctor (α → ·) where - map_const := by solve_by_elim - id_map := by simp - comp_map := by simp [Function.comp_assoc] - - /-- Yoneda forward map -/ - def yoneda (g : {β : Type u} → (α → β) → m β) [Functor m] [LawfulFunctor m] : m α := g id - - /-- Yoneda reverse map -/ - def yoneda' [Functor m] [LawfulFunctor m] (y : m α) : {β : Type u} → (α → β) → m β := (· <$> y) - - /-- Reverse map always produces a natural transformation -/ - instance [Functor m] [LawfulFunctor m] : Natural (α → ·) m (yoneda' y) where - naturality x h := by simp [yoneda']; rfl - - /-- Mapping and unmapping a natural transformation returns the itself - - Note that this does work for an arbitrary function between the hom-functor and `m` because we use the naturality condition. -/ - theorem yoneda_lemma (g : {β : Type u} → (α → β) → m β) [Functor m] [LawfulFunctor m] [N : Natural (α → ·) m g] - : (yoneda' (β := ·) (yoneda (m := m) g)) = (g (β := ·)) := by - unfold yoneda yoneda' - simp [N.naturality] - - /-- Mapping and unmapping an element `m α` returns itself -/ - theorem yoneda_lemma' (y : m α) [Functor m] [LawfulFunctor m] - : yoneda (yoneda' (m := m) (α := α) y) = y := by - simp [yoneda, yoneda'] - - end Yoneda