reid.lean

import topology.compact_open
import category_theory.closed.cartesian
import topology.category.Top
import category_theory.limits.shapes

open_locale topological_space
namespace category_theory
open limits

universes v u

def top_prod_left (α : Type u) [topological_space α] : Top.{u} ⥤ Top.{u} :=
{ obj := λ β, Top.of (α × β.α),
  map := λ β β' f, ⟨_, continuous.prod_map continuous_id f.2⟩ }

def top_prod_right (α : Type u) [topological_space α] : Top.{u} ⥤ Top.{u} :=
{ obj := λ β, Top.of (β.α × α),
  map := λ β β' f, ⟨_, continuous.prod_map f.2 continuous_id⟩ }

def swap_prod (α : Type u) [topological_space α] : top_prod_left α ≅ top_prod_right α :=
nat_iso.of_components
(λ β, { hom := ⟨_, continuous_swap⟩, inv := ⟨_, continuous_swap⟩ })
(by tidy)

def nice_prod {α : Type u} [topological_space α] :
  top_prod_left α ≅ prod_functor.obj (Top.of α) :=
nat_iso.of_components
(λ β,
{ hom := limits.prod.lift ⟨_, continuous_fst⟩ ⟨_, continuous_snd⟩,
  inv := ⟨_, continuous.prod_mk (limits.prod.fst : _ ⨯ β ⟶ _).2 (limits.prod.snd : _ ⨯ β ⟶ _).2⟩ })
(by tidy)

def nice_prod' {α : Type u} [topological_space α] :
  top_prod_right α ≅ prod_functor.obj (Top.of α) :=
(swap_prod α).symm ≪≫ nice_prod

variables {α : Type u} [topological_space α] [locally_compact_space α]

instance exp_local_compact :
  exponentiable (Top.of α) :=
{ is_adj :=
  { right :=
    { obj := λ β, Top.of (continuous_map α β.α),
      map := λ β γ f, ⟨_, continuous_map.continuous_induced f.2⟩ },
    adj :=
    begin
      apply adjunction.of_nat_iso_left _ nice_prod',
      apply adjunction.mk_of_unit_counit,
      exact { unit := {app := λ β, ⟨_, continuous_map.continuous_coev⟩ },
              counit := {app := λ β, ⟨_, continuous_map.continuous_ev⟩ }}
    end } }.

instance prod_preserves_colimits : preserves_colimits (prod_functor.obj (Top.of α)) :=
adjunction.left_adjoint_preserves_colimits (exp.adjunction _)

def prod_colimit_iso {β γ δ : Top.{u}} (f : β ⟶ γ) (g : β ⟶ δ) :
  Top.of α ⨯ pushout f g ≅ pushout (limits.prod.map (𝟙 (Top.of α)) f) (limits.prod.map (𝟙 (Top.of α)) g) :=
begin
  apply preserves_colimit_iso (span f g) (prod_functor.obj (Top.of α)) ≪≫ _,
  apply has_colimit.iso_of_nat_iso,
  exact diagram_iso_span (span f g ⋙ prod_functor.obj (Top.of α)),
end

end category_theory