import topology.category.Profinite
import category_theory.limits.shapes.products
/-!
In this file we show that a finite disjoint union of profinite sets agrees with the coproduct.
Note: The existence of the coproduct is currently shown using some abstract nonsense.
-/
namespace topology
lemma is_preconnected.preimage : Prop := sorry
lemma sigma.univ {α : Type} (X : α → Type) :
(set.univ : set (Σ a, X a)) = ⋃ a, sigma.mk _ '' (set.univ : set (X a)) :=
by { ext, simp only [set.image_univ, set.mem_preimage, set.mem_Union, set.mem_univ,
set.mem_singleton_iff, set.range_sigma_mk, exists_eq'] }
lemma sigma.is_connected_iff {α : Type} {X : α → Type} [∀ a, topological_space (X a)]
{s : set (Σ a, X a)} :
is_connected s ↔ ∃ (a : α) (t : set (X a)), is_connected t ∧ s = sigma.mk _ '' t :=
begin
refine ⟨λ hs, _, _⟩,
{ obtain ⟨⟨a, x⟩, hx⟩ := hs.nonempty,
refine ⟨a, sigma.mk a ⁻¹' s, ⟨⟨x, hx⟩, _⟩, _⟩,
sorry,
sorry
},
{ rintro ⟨a, t, ht, rfl⟩,
exact ht.image _ continuous_sigma_mk.continuous_on }
end
lemma sigma.is_preconnected_iff {α : Type} [hα : nonempty α] {X : α → Type}
[∀ a, topological_space (X a)] {s : set (Σ a, X a)} :
is_preconnected s ↔ ∃ (a : α) (t : set (X a)), is_preconnected t ∧ s = sigma.mk _ '' t :=
begin
refine ⟨λ hs, _, _⟩,
{
obtain rfl | h := s.eq_empty_or_nonempty,
{ obtain a := hα,
have := hα.elim,
refine ⟨hα.elim _, ∅, _, _⟩, -- weird state here
exact set.subsingleton_empty },
obtain ⟨⟨a, x⟩, hx⟩ := h,
refine ⟨a, sigma.mk a ⁻¹' s, _, _⟩,
sorry
},
{ rintro ⟨a, t, ht, rfl⟩,
exact ht.image _ continuous_sigma_mk.continuous_on }
end
end topology
namespace Profinite
universe u
variables {α : Type u} [fintype α] (X : α → Profinite.{u})
def sum.desc {Z} (X Y : Profinite.{u}) (f : X ⟶ Z) (g : Y ⟶ Z) : sum X Y ⟶ Z :=
{ to_fun := λ x, _root_.sum.rec_on x f g,
continuous_to_fun := begin
apply continuous_sup_dom,
{ apply continuous_coinduced_dom, exact f.continuous },
{ apply continuous_coinduced_dom, exact g.continuous }
end }
def sigma : Profinite.{u} :=
Profinite.of $ Σ a, X a
def sigma.ι (a : α) : X a ⟶ sigma X :=
{ to_fun := λ t, ⟨_,t⟩,
continuous_to_fun := sorry }
def sigma.desc {Y} (f : Π a, X a ⟶ Y) : sigma X ⟶ Y :=
{ to_fun := λ ⟨a,t⟩, f a t,
continuous_to_fun := sorry }
open category_theory
def sigma_cofan : limits.cofan X :=
limits.cofan.mk (sigma X) (sigma.ι X)
def sigma_cofan_is_colimit : limits.is_colimit (sigma_cofan X) :=
{ desc := λ S, sigma.desc _ $ λ a, S.ι.app a,
uniq' := begin
intros S m h,
apply sigma.hom_ext,
intros a,
convert h a,
simp,
end }
end Profinite