cat_ramsey.lean

import data.finset
import category_theory.category
import category_theory.isomorphism

namespace category_theory
open set category_theory.category

universes v u

/-- A partition of the type s into finitely many bits -/
structure partition (s : Type*) :=
(sets : finset (set s)) -- The collection of sets in the partition
(disjoint : ∀ (i j ∈ sets), i = j ∨ i ∩ j = ∅) -- Any two sets are disjoint or equal
(everything : ∀ (x : s), ∃ i ∈ sets, x ∈ i) -- Everything is in something of the partition

def partition.card {s : Type*} (p : partition s) : ℕ := finset.card p.sets
instance {s : Type*} : has_mem (set s) (partition s) := ⟨λ s p, s ∈ p.sets⟩

lemma unique_membership (s : Type*) (p : partition s) (x : s) :
  ∃! (i ∈ p.sets), x ∈ i :=
sorry

variables {C : Type u} [category.{v} C]

def aut (A : C) : set (A ⟶ A) :=
λ f, nonempty (is_iso f)

def rigid (A : C) : Prop := aut A = {𝟙 _}

lemma rigid_iff_subset (A : C) : rigid A ↔ aut A ⊆ {𝟙 _} :=
sorry

def relate (A : C) {B : C} (f f' : A ⟶ B) : Prop := ∃ α ∈ aut A, α ≫ f = f'

instance cancelling (A B : C) : setoid (A ⟶ B) :=
{ r := relate A,
  iseqv := sorry }

def cancel_isos (A B : C) := quotient (category_theory.cancelling A B)

def act_on_cancel {A B c : C} (w : B ⟶ c) (f : cancel_isos A B) : cancel_isos A c :=
sorry

def big_arrow (A B c : C) (k : ℕ) : Prop :=
nonempty (A ⟶ B) ∧ nonempty (B ⟶ c) ∧ ∀ (p : partition (cancel_isos A c)), p.card = k → ∃ (s ∈ p) (w : B ⟶ c), (set.range (act_on_cancel w) ⊆ s)

def big_hom_arrow (A B c : C) (k : ℕ) : Prop :=
nonempty (A ⟶ B) ∧ nonempty (B ⟶ c) ∧ ∀ (p : partition (A ⟶ c)), p.card = k → ∃ (s ∈ p) (w : B ⟶ c), (set.range (≫ w) ⊆ s)

variable (C)
def object_ramsey : Prop := ∀ {A B : C} {k}, 2 ≤ k → nonempty (A ⟶ B) → ∃ c, big_arrow A B c k
def morphism_ramsey : Prop := ∀ {A B : C} {k}, 2 ≤ k → nonempty (A ⟶ B) → ∃ c, big_hom_arrow A B c k

section prop_two_three

-- Assume all morphisms are monic
variable (all_mon : ∀ {A B : C} (f : A ⟶ B), mono f)

theorem part_one (h : morphism_ramsey C) (A : C) : rigid A :=
sorry

theorem part_two : morphism_ramsey C ↔ (∀ (A : C), rigid A) ∧ object_ramsey C :=
sorry

end prop_two_three

section easy_lemmas

lemma four_a {A B B₁ c : C} {k : ℕ} (h : big_hom_arrow A B c k) [nonempty (B₁ ⟶ B)] :
  big_hom_arrow A B₁ c k :=
sorry

lemma four_b {A B B₁ c : C} {k : ℕ} (h : big_arrow A B c k) [nonempty (B₁ ⟶ B)] :
  big_arrow A B₁ c k :=
sorry

end easy_lemmas
end category_theory