category.lean

import category_theory.concrete_category.bundled_hom
import topology.category.Profinite
import data.equiv.fin
import for_mathlib.concrete
import for_mathlib.CompHaus

import pseudo_normed_group.with_Tinv

/-!

# The category of profinitely filtered pseudo-normed groups.

The category of profinite pseudo-normed groups, and the category of
profinitely filtered pseudo-normed groups equipped with an action of T⁻¹.

-/
universe variables u

open category_theory
open_locale nnreal

local attribute [instance] type_pow

noncomputable theory

/-- The category of CompHaus-ly filtered pseudo-normed groups. -/
def CompHausFiltPseuNormGrp : Type (u+1) :=
bundled comphaus_filtered_pseudo_normed_group

namespace CompHausFiltPseuNormGrp

def bundled_hom : bundled_hom @comphaus_filtered_pseudo_normed_group_hom :=
⟨@comphaus_filtered_pseudo_normed_group_hom.to_fun,
 @comphaus_filtered_pseudo_normed_group_hom.id,
 @comphaus_filtered_pseudo_normed_group_hom.comp,
 @comphaus_filtered_pseudo_normed_group_hom.coe_inj⟩

local attribute [instance] bundled_hom
attribute [derive [has_coe_to_sort, large_category, concrete_category]] CompHausFiltPseuNormGrp

instance (M : CompHausFiltPseuNormGrp) : comphaus_filtered_pseudo_normed_group M := M.str

/-- Construct a bundled `CompHausFiltPseuNormGrp` from the underlying type and typeclass. -/
def of (M : Type u) [comphaus_filtered_pseudo_normed_group M] : CompHausFiltPseuNormGrp :=
bundled.of M

end CompHausFiltPseuNormGrp

/-- The category of CompHaus-ly filtered pseudo-normed groups with strict morphisms. -/
structure CompHausFiltPseuNormGrp₁ : Type (u+1) :=
(M : Type u)
[str : comphaus_filtered_pseudo_normed_group M]
(exhaustive' : ∀ m : M, ∃ c, m ∈ pseudo_normed_group.filtration M c)


namespace CompHausFiltPseuNormGrp₁

instance : has_coe_to_sort CompHausFiltPseuNormGrp₁ := ⟨Type*, λ M, M.M⟩
instance (M : CompHausFiltPseuNormGrp₁) : comphaus_filtered_pseudo_normed_group M := M.str

lemma exhaustive (M : CompHausFiltPseuNormGrp₁) (m : M) :
  ∃ c, m ∈ pseudo_normed_group.filtration M c := M.exhaustive' _

/-
def bundled_hom : bundled_hom @strict_comphaus_filtered_pseudo_normed_group_hom :=
⟨@strict_comphaus_filtered_pseudo_normed_group_hom.to_fun,
 @strict_comphaus_filtered_pseudo_normed_group_hom.id,
 @strict_comphaus_filtered_pseudo_normed_group_hom.comp,
 @strict_comphaus_filtered_pseudo_normed_group_hom.coe_inj⟩

local attribute [instance] bundled_hom
attribute [derive [has_coe_to_sort, large_category, concrete_category]] CompHausFiltPseuNormGrp₁
-/

instance : large_category CompHausFiltPseuNormGrp₁.{u} :=
{ hom := λ A B, strict_comphaus_filtered_pseudo_normed_group_hom A B,
  id := λ A, strict_comphaus_filtered_pseudo_normed_group_hom.id,
  comp := λ A B C f g, g.comp f }

def enlarging_functor : CompHausFiltPseuNormGrp₁ ⥤ CompHausFiltPseuNormGrp :=
{ obj := λ M, CompHausFiltPseuNormGrp.of M,
  map := λ M₁ M₂ f, f.to_chfpsng_hom }

instance : concrete_category CompHausFiltPseuNormGrp₁.{u} :=
{ forget :=
  { obj := λ M, M.M,
    map := λ A B f, f },
  forget_faithful := ⟨⟩ } .

def level : ℝ≥0 ⥤ CompHausFiltPseuNormGrp₁.{u} ⥤ CompHaus :=
{ obj := λ c,
  { obj := λ M, CompHaus.of $ pseudo_normed_group.filtration M c,
    map := λ A B f, ⟨_, f.level_continuous _⟩ },
  map := λ c₁ c₂ h,
    { app := λ M, by letI : fact (c₁ ≤ c₂) := ⟨le_of_hom h⟩; exact
        ⟨_, comphaus_filtered_pseudo_normed_group.continuous_cast_le _ _⟩ } } .

section limits

/-!
In this section, we show (hopefully ;)) that `CompHausFiltPseuNormGrp₁` has limits.
-/

variables {J : Type u} [small_category J] (G : J ⥤ CompHausFiltPseuNormGrp₁.{u})

open pseudo_normed_group
open category_theory.limits

/-- This is a bifunctor which associates to each `c : ℝ≥0` and `j : J`,
  the `c`-th term of the filtration of `G.obj j`. -/
def cone_point_diagram : as_small.{u} ℝ≥0 ⥤ J ⥤ CompHaus.{u} :=
as_small.down ⋙ level ⋙ (whiskering_left _ _ _).obj G

@[derive [topological_space, t2_space]]
def cone_point_type_filt (c : ℝ≥0) : Type u :=
{ x : Π j : J, filtration (G.obj j) c | ∀ ⦃i j : J⦄ (e : i ⟶ j), (G.map e).level (x _) = x _ }

instance (c : ℝ≥0) : compact_space (cone_point_type_filt G c) :=
(CompHaus.limit_cone (((cone_point_diagram G).obj (as_small.up.obj c)))).X.is_compact -- ;-)

namespace cone_point_type_filt

variable {G}

instance (c : ℝ≥0) : has_coe_to_fun (cone_point_type_filt G c) :=
⟨λ x, Π j : J, filtration (G.obj j) c, λ x, x.1⟩

@[ext] lemma ext {c} (x y : cone_point_type_filt G c) : ⇑x = y → x = y := subtype.ext

@[simp] lemma level_apply {c : ℝ≥0} {i j : J} (x : cone_point_type_filt G c) (e : i ⟶ j) :
  (G.map e).level (x i) = x j := x.2 e

def trans {c₁ c₂ : ℝ≥0} (h : c₁ ≤ c₂) (x : cone_point_type_filt G c₁) : cone_point_type_filt G c₂ :=
⟨λ j, cast_le' h (x j), λ i j e, by { ext, simp }⟩

@[simp] lemma trans_apply {c₁ c₂ : ℝ≥0} (h : c₁ ≤ c₂) (x : cone_point_type_filt G c₁) (j : J) :
  x.trans h j = cast_le' h (x j) := by { ext, refl }

lemma trans_injective {c₁ c₂ : ℝ≥0} (h : c₁ ≤ c₂) :
  function.injective (trans h : cone_point_type_filt G c₁ → cone_point_type_filt G c₂) :=
begin
  intros x y hh,
  ext j,
  apply_fun (λ e, (e j : G.obj j)) at hh,
  exact hh
end

lemma trans_continuous {c₁ c₂ : ℝ≥0} (h : c₁ ≤ c₂) :
  continuous (trans h : cone_point_type_filt G c₁ → cone_point_type_filt G c₂) :=
begin
  -- ;-)
  let η := ((cone_point_diagram G).map (as_small.up.map $ hom_of_le $ h)),
  let hS := (CompHaus.limit_cone_is_limit (((cone_point_diagram G).obj (as_small.up.obj c₂)))),
  let T := (CompHaus.limit_cone (((cone_point_diagram G).obj (as_small.up.obj c₁)))),
  exact (hS.map T η).continuous,
end

lemma continuous_apply {c : ℝ≥0} (j : J) : continuous (λ t : cone_point_type_filt G c, t j) :=
begin
  change continuous ((λ u : Π j, filtration (G.obj j) c, u j) ∘
    (λ u : cone_point_type_filt G c, ⇑u)),
  apply continuous.comp,
  apply continuous_apply,
  apply continuous_subtype_coe,
end

instance {c} : has_zero (cone_point_type_filt G c) := has_zero.mk $
⟨λ j, 0, λ i j e, by { ext, dsimp, simp }⟩

instance {c} : has_neg (cone_point_type_filt G c) := has_neg.mk $ λ x,
⟨λ j, - (x j), λ i j e, by { ext, dsimp, simp }⟩

def add' {c₁ c₂} (x : cone_point_type_filt G c₁) (y : cone_point_type_filt G c₂) :
  cone_point_type_filt G (c₁ + c₂) :=
⟨λ j, add' (x j, y j), λ i j e, by { ext, dsimp, simp }⟩

@[simp] lemma zero_apply {c} (j : J) : (0 : cone_point_type_filt G c) j = 0 := rfl
@[simp] lemma neg_apply {c} (j : J) (x : cone_point_type_filt G c) : (-x) j = - (x j) := rfl
@[simp] lemma add'_apply_coe {c₁ c₂} (j : J) (x : cone_point_type_filt G c₁)
  (y : cone_point_type_filt G c₂) : ((x.add' y) j : G.obj j) = x j + y j := rfl

lemma continuous_neg {c} : continuous (λ x : cone_point_type_filt G c, - x) :=
begin
  apply continuous_subtype_mk,
  apply continuous_pi,
  intros j,
  change continuous ((λ x, -x) ∘ (λ a : cone_point_type_filt G c, (a j))),
  apply continuous.comp,
  apply comphaus_filtered_pseudo_normed_group.continuous_neg',
  apply continuous_apply,
end

lemma continuous_add' {c1 c2} :
  continuous (λ t : cone_point_type_filt G c1 × cone_point_type_filt G c2, t.1.add' t.2) :=
begin
  apply continuous_subtype_mk,
  apply continuous_pi,
  intros j,
  let A : cone_point_type_filt G c1 × cone_point_type_filt G c2 →
    (Π j : J, filtration (G.obj j) c1) × (Π j : J, filtration (G.obj j) c2) :=
    λ t, (t.1,t.2),
  let B : (Π j : J, filtration (G.obj j) c1) × (Π j : J, filtration (G.obj j) c2) →
    filtration (G.obj j) c1 × filtration (G.obj j) c2 := λ t, (t.1 j, t.2 j),
  let C : filtration (G.obj j) c1 × filtration (G.obj j) c2 → filtration (G.obj j) (c1 + c2) :=
    pseudo_normed_group.add',
  change continuous (C ∘ B ∘ A),
  apply continuous.comp,
  apply comphaus_filtered_pseudo_normed_group.continuous_add',
  apply continuous.comp,
  { apply continuous.prod_mk,
    { change continuous ((λ t : Π j : J, filtration (G.obj j) c1, t j) ∘ prod.fst),
      apply continuous.comp,
      apply _root_.continuous_apply,
      exact continuous_fst },
    { change continuous ((λ t : Π j : J, filtration (G.obj j) c2, t j) ∘ prod.snd),
      apply continuous.comp,
      apply _root_.continuous_apply,
      exact continuous_snd } },
  apply continuous.prod_map,
  apply continuous_subtype_coe,
  apply continuous_subtype_coe,
end

end cone_point_type_filt

def cone_point_type_setoid : setoid (Σ (c : ℝ≥0), cone_point_type_filt G c) :=
{ r := λ x y, ∃ (d : ℝ≥0) (hx : x.1 ≤ d) (hy : y.1 ≤ d), x.2.trans hx = y.2.trans hy,
  iseqv := begin
    refine ⟨_,_,_⟩,
    { rintro ⟨c,x⟩,
      use [c, le_refl _, le_refl _] },
    { rintro ⟨c,x⟩ ⟨d,y⟩ ⟨e,h1,h2,h⟩,
      dsimp at *,
      refine ⟨_, le_sup_left, le_sup_right, _⟩,
      ext j : 3,
      symmetry,
      apply_fun (λ e, (e j : G.obj j)) at h,
      exact h },
    { rintro ⟨c,x⟩ ⟨d,y⟩ ⟨e,z⟩ ⟨i,h1,hh1,hhh1⟩ ⟨j,h2,hh2,hhh2⟩,
      dsimp at *,
      refine ⟨_, le_sup_left, le_sup_right, _⟩,
      ext jj : 3,
      apply_fun (λ e, (e jj : G.obj jj)) at hhh1,
      apply_fun (λ e, (e jj : G.obj jj)) at hhh2,
      erw [hhh1, hhh2], refl },
  end }

def cone_point_type : Type u := quotient (cone_point_type_setoid G)

namespace cone_point_type
variable {G}

def incl (c : ℝ≥0) : cone_point_type_filt G c → cone_point_type G :=
quotient.mk' ∘ sigma.mk c

lemma incl_injective (c : ℝ≥0) :
  function.injective (incl c : cone_point_type_filt G c → cone_point_type G) :=
begin
  intros x y h,
  replace h := quotient.exact' h,
  obtain ⟨d,h1,h2,h⟩ := h,
  dsimp at h1 h2 h,
  rw (show h1 = h2, by refl) at h,
  apply cone_point_type_filt.trans_injective h2,
  exact h,
end

@[simp]
lemma incl_trans {c₁ c₂ : ℝ≥0} (h : c₁ ≤ c₂) (x : cone_point_type_filt G c₁) :
  incl _ (x.trans h) = incl _ x :=
begin
  apply quotient.sound',
  refine ⟨c₁ ⊔ c₂, by simp, by simp, _⟩,
  ext,
  refl,
end

lemma incl_jointly_surjective (x : cone_point_type G) :
  ∃ (c : ℝ≥0) (y : cone_point_type_filt G c), incl c y = x :=
begin
  rcases x,
  obtain ⟨c,y⟩ := x,
  use [c,y],
  refl,
end

def index (x : cone_point_type G) : ℝ≥0 := (incl_jointly_surjective x).some

def preimage (x : cone_point_type G) : cone_point_type_filt G x.index :=
  (incl_jointly_surjective x).some_spec.some

@[simp]
lemma preimage_spec (x : cone_point_type G) : incl _ x.preimage = x :=
  (incl_jointly_surjective x).some_spec.some_spec

@[simp]
lemma coe_incl_preimage_apply {c} (x : cone_point_type_filt G c) (j : J) :
  ((incl c x).preimage j : G.obj j) = x j :=
begin
  let e := c ⊔ (incl c x).index,
  change _ = (cast_le' le_sup_left (x j) : G.obj j),
  rw ← cone_point_type_filt.trans_apply (le_sup_left : _ ≤ e) x j,
  rw ← coe_cast_le' (le_sup_right : _ ≤ e),
  rw ← cone_point_type_filt.trans_apply,
  congr' 2,
  apply incl_injective,
  simp,
end


instance : has_zero (cone_point_type G) := ⟨incl 0 0⟩

lemma zero_def : (0 : cone_point_type G) = incl 0 0 := rfl

instance : has_neg (cone_point_type G) := has_neg.mk $
λ x, incl _ (-x.preimage)

lemma neg_def (x : cone_point_type G) : -x = incl _ (-x.preimage) := rfl

instance : has_add (cone_point_type G) := has_add.mk $
λ x y, incl _ (x.preimage.add' y.preimage)

lemma add_def (x y : cone_point_type G) : x + y = incl _ (x.preimage.add' y.preimage) := rfl

lemma zero_add (x : cone_point_type G) : 0 + x = x :=
begin
  conv_rhs {rw ← x.preimage_spec},
  apply quotient.sound',
  refine ⟨(0 : cone_point_type G).index + x.index, by simp, by simp, _⟩,
  dsimp,
  ext j : 3,
  simp only [cone_point_type_filt.trans_apply, cone_point_type_filt.add'_apply_coe, coe_cast_le'],
  simp only [add_left_eq_self],
  apply coe_incl_preimage_apply,
end

lemma add_comm (x y : cone_point_type G) : x + y = y + x :=
begin
  apply quotient.sound',
  refine ⟨x.index + y.index, le_refl _, le_of_eq (by {dsimp, rw add_comm}), _⟩,
  dsimp,
  ext j : 3,
  simp only [cone_point_type_filt.trans_apply, cone_point_type_filt.add'_apply_coe,
    coe_cast_le, coe_cast_le'],
  rw add_comm,
end

lemma add_zero (x : cone_point_type G) : x + 0 = x := by { rw add_comm, apply zero_add }

lemma add_assoc (x y z : cone_point_type G) : x + y + z = x + (y + z) :=
begin
  apply quotient.sound',
  refine ⟨_, le_sup_left, le_sup_right, _⟩,
  dsimp,
  ext j : 3,
  simp only [cone_point_type_filt.trans_apply, cone_point_type_filt.add'_apply_coe,
    coe_cast_le, coe_cast_le'],
  erw [coe_incl_preimage_apply, coe_incl_preimage_apply],
  simp [add_assoc],
end

lemma add_left_neg (x : cone_point_type G) : -x + x = 0 :=
begin
  apply quotient.sound',
  refine ⟨_,le_sup_left, le_sup_right,_⟩,
  dsimp,
  ext j : 3,
  simp only [cone_point_type_filt.trans_apply, cone_point_type_filt.zero_apply,
    cone_point_type_filt.add'_apply_coe, coe_cast_le, filtration.coe_zero, coe_cast_le'],
  erw coe_incl_preimage_apply,
  simp,
end

instance : add_comm_group (cone_point_type G) :=
{ add_assoc := add_assoc,
  zero_add := zero_add,
  add_zero := add_zero,
  add_left_neg := add_left_neg,
  add_comm := add_comm,
  ..(infer_instance : has_add _),
  ..(infer_instance : has_zero _),
  ..(infer_instance : has_neg _) }

variable (G)
def filt (c : ℝ≥0) : set (cone_point_type G) := set.range (incl c)

def filt_equiv (c : ℝ≥0) : cone_point_type_filt G c ≃ filt G c :=
equiv.of_bijective (λ x, ⟨_, x, rfl⟩)
begin
  split,
  { intros x y h,
    apply_fun (λ e, e.val) at h,
    apply incl_injective,
    exact h },
  { rintro ⟨_,x,rfl⟩, use x }
end

instance {c} : topological_space (filt G c) :=
topological_space.induced (filt_equiv G c).symm infer_instance

def filt_homeo (c : ℝ≥0) : filt G c ≃ₜ cone_point_type_filt G c :=
homeomorph.homeomorph_of_continuous_open (filt_equiv G c).symm continuous_induced_dom
begin
  intros U hU,
  have : inducing (filt_equiv G c).symm := ⟨rfl⟩,
  rw this.is_open_iff at hU,
  obtain ⟨U,hU,rfl⟩ := hU,
  simpa,
end

instance {c} : compact_space (filt G c) :=
(filt_homeo G c).symm.compact_space

instance {c} : t2_space (filt G c) :=
(filt_homeo G c).symm.t2_space

variable {G}

@[simp] lemma incl_neg {c} (x : cone_point_type_filt G c) :
  incl c (-x) = - incl c x :=
begin
  apply quotient.sound',
  refine ⟨_, le_sup_left, le_sup_right, _⟩,
  dsimp,
  ext j : 3,
  simp,
end

@[simp] lemma incl_add' {c1 c2} (x1 : cone_point_type_filt G c1) (x2 : cone_point_type_filt G c2) :
  incl (c1 + c2) (x1.add' x2) = incl c1 x1 + incl c2 x2 :=
begin
  apply quotient.sound',
  refine ⟨_, le_sup_left, le_sup_right, _⟩,
  dsimp,
  ext j : 3,
  simp,
end

@[simp] lemma incl_zero {c} : incl c (0 : cone_point_type_filt G c) = 0 :=
begin
  apply quotient.sound',
  refine ⟨_, le_sup_left, le_sup_right, _⟩,
  dsimp,
  ext j : 3,
  simp,
end

instance : pseudo_normed_group (cone_point_type G) :=
{ filtration := filt G,
  filtration_mono := begin
    rintro c1 c2 h x ⟨x,rfl⟩,
    dsimp [filt],
    use x.trans h,
    simp,
  end,
  zero_mem_filtration := begin
    intro c,
    use 0,
    simp,
  end,
  neg_mem_filtration := begin
    rintros c x ⟨x,rfl⟩,
    use -x,
    simp,
  end,
  add_mem_filtration := begin
    rintros c1 c2 x1 x2 ⟨x1,rfl⟩ ⟨x2,rfl⟩,
    use x1.add' x2,
    simp,
  end }

instance : comphaus_filtered_pseudo_normed_group (cone_point_type G) :=
{ topology := by apply_instance,
  t2 := by apply_instance,
  compact := by apply_instance,
  continuous_add' := begin
    intros c1 c2,
    let E : filtration (cone_point_type G) c1 × filtration (cone_point_type G) c2 →
      cone_point_type_filt G c1 × cone_point_type_filt G c2 :=
      λ t, ⟨(filt_homeo G c1) t.1, (filt_homeo G c2) t.2⟩,
    let E' : cone_point_type_filt G c1 × cone_point_type_filt G c2 →
      filtration (cone_point_type G) c1 × filtration (cone_point_type G) c2 :=
      λ t, ⟨(filt_homeo G c1).symm t.1, (filt_homeo G c2).symm t.2⟩,
    have hE'E : E' ∘ E = id := by { dsimp [E,E'], ext, simp, simp },
    have : (filt_homeo G (c1 + c2)).symm ∘
      (λ t : cone_point_type_filt G c1 × cone_point_type_filt G c2, t.1.add' t.2) ∘ E = add',
    { suffices : add' ∘ E' = (filt_homeo G (c1 + c2)).to_equiv.symm ∘
        (λ t : cone_point_type_filt G c1 × cone_point_type_filt G c2, t.1.add' t.2),
      { erw [← function.comp.assoc, ← this, function.comp.assoc, hE'E],
        simp },
      dsimp only [filt_homeo, homeomorph.homeomorph_of_continuous_open, E'],
      ext,
      dsimp [filt_homeo, filt_equiv, E, E'],
      simp },
    rw ← this, clear this,
    apply continuous.comp (homeomorph.continuous _),
    apply continuous.comp,
    apply cone_point_type_filt.continuous_add',
    dsimp [E],
    continuity,
  end,
  continuous_neg' := begin
    intros c,
    have : (neg' : filtration (cone_point_type G) c → filtration (cone_point_type G) c) =
      (filt_homeo G c).symm ∘ (λ x, -x) ∘ filt_homeo G c,
    { suffices :
        (neg' : filtration (cone_point_type G) c → filtration (cone_point_type G) c) ∘
          (filt_homeo G c).to_equiv.symm = (filt_homeo G c).to_equiv.symm ∘ (λ x, -x),
      { erw [← function.comp.assoc, ← this, function.comp.assoc, equiv.symm_comp_self],
        simp },
      dsimp only [filt_homeo, homeomorph.homeomorph_of_continuous_open],
      simp only [equiv.symm_symm],
      ext,
      dsimp [filt_equiv],
      simp },
    rw this,
    simp [cone_point_type_filt.continuous_neg],
  end,
  continuous_cast_le := begin
    rintro c₁ c₂ ⟨h⟩,
    change continuous (cast_le' h),
    have : cast_le' h = (filt_homeo G c₂).symm ∘
      cone_point_type_filt.trans h ∘ (filt_homeo G c₁),
    { suffices : cast_le' h ∘ (filt_homeo G c₁).to_equiv.symm =
        (filt_homeo G c₂).to_equiv.symm ∘ cone_point_type_filt.trans h,
      { erw [← function.comp.assoc, ← this, function.comp.assoc, equiv.symm_comp_self],
        simp },
      dsimp only [filt_homeo, homeomorph.homeomorph_of_continuous_open],
      simp only [equiv.symm_symm],
      ext,
      dsimp [filt_equiv],
      simp },
    simp [this, cone_point_type_filt.trans_continuous],
  end }

end cone_point_type

def cone_point : CompHausFiltPseuNormGrp₁ :=
{ M := cone_point_type G,
  exhaustive' := cone_point_type.incl_jointly_surjective }

def proj (j : J) : cone_point G ⟶ G.obj j :=
{ to_fun := λ x, x.preimage j,
  map_zero' := begin
    rw cone_point_type.zero_def,
    simp only [cone_point_type.coe_incl_preimage_apply,
      cone_point_type_filt.zero_apply, filtration.coe_zero],
  end,
  map_add' := begin
    intros x y,
    rw cone_point_type.add_def x y,
    simp only [cone_point_type.coe_incl_preimage_apply,
      cone_point_type_filt.add'_apply_coe],
  end,
  strict' := begin
    rintros c x ⟨x,rfl⟩,
    simp only [cone_point_type.coe_incl_preimage_apply,
      subtype.coe_prop],
  end,
  continuous₁' := begin
    intros c,
    dsimp,
    let E : filtration (cone_point_type G) c → filtration (G.obj j) c :=
      λ t, ((cone_point_type.filt_homeo G c) t) j,
    suffices : continuous E,
    { convert this,
      ext ⟨t,t,rfl⟩,
      dsimp [E],
      simp only [cone_point_type.coe_incl_preimage_apply],
      congr' 2,
      apply_fun (cone_point_type.filt_homeo G c).symm,
      simp only [homeomorph.symm_apply_apply],
      ext, refl },
    dsimp [E],
    change continuous ((λ (u : cone_point_type_filt G c), u j) ∘ cone_point_type.filt_homeo G c),
    simp only [homeomorph.comp_continuous_iff'],
    apply cone_point_type_filt.continuous_apply,
  end } .

def limit_cone : cone G :=
{ X := cone_point G,
  π :=
  { app := λ j, proj G j,
    naturality' := begin
      intros i j e,
      ext,
      dsimp,
      simp only [comp_apply, category.id_comp],
      have := (cone_point_type.preimage x).2 e,
      apply_fun (λ e, (e : G.obj j)) at this,
      exact this.symm,
    end } }

def index {M : CompHausFiltPseuNormGrp₁} (x : M) : ℝ≥0 := (M.exhaustive x).some
def preimage {M : CompHausFiltPseuNormGrp₁} (x : M) : filtration M (index x) :=
  ⟨x,(M.exhaustive x).some_spec⟩

def limit_cone_lift (D : cone G) : D.X ⟶ cone_point G :=
{ to_fun := λ x, cone_point_type.incl (index x)
    ⟨λ j, (D.π.app j).level (preimage x), sorry⟩,
  map_zero' := sorry,
  map_add' := sorry,
  strict' := sorry,
  continuous₁' := sorry }

def limit_cone_is_limit : is_limit (limit_cone G) :=
{ lift := λ S, limit_cone_lift _ _,
  fac' := sorry,
  uniq' := sorry }

-- This is the goal of this section...
instance : has_limit G := has_limit.mk ⟨limit_cone _, limit_cone_is_limit _⟩

instance : has_limits CompHausFiltPseuNormGrp₁ :=
⟨λ J hJ, { has_limit := λ G, by resetI; apply_instance }⟩

end limits

end CompHausFiltPseuNormGrp₁

/-- The category of profinitely filtered pseudo-normed groups. -/
def ProFiltPseuNormGrp : Type (u+1) :=
bundled profinitely_filtered_pseudo_normed_group

/-- The category of profinitely filtered pseudo-normed groups with action of `T⁻¹`. -/
def ProFiltPseuNormGrpWithTinv (r : ℝ≥0) : Type (u+1) :=
bundled (@profinitely_filtered_pseudo_normed_group_with_Tinv r)

namespace ProFiltPseuNormGrp

local attribute [instance] CompHausFiltPseuNormGrp.bundled_hom

def bundled_hom : bundled_hom.parent_projection
  @profinitely_filtered_pseudo_normed_group.to_comphaus_filtered_pseudo_normed_group := ⟨⟩

local attribute [instance] bundled_hom

attribute [derive [has_coe_to_sort, large_category, concrete_category]] ProFiltPseuNormGrp

instance : has_forget₂ ProFiltPseuNormGrp CompHausFiltPseuNormGrp := bundled_hom.forget₂ _ _

@[simps]
def to_CompHausFilt : ProFiltPseuNormGrp ⥤ CompHausFiltPseuNormGrp := forget₂ _ _

/-- Construct a bundled `ProFiltPseuNormGrp` from the underlying type and typeclass. -/
def of (M : Type u) [profinitely_filtered_pseudo_normed_group M] : ProFiltPseuNormGrp :=
bundled.of M

instance : has_zero ProFiltPseuNormGrp := ⟨of punit⟩

instance : inhabited ProFiltPseuNormGrp := ⟨0⟩

instance (M : ProFiltPseuNormGrp) : profinitely_filtered_pseudo_normed_group M := M.str

@[simp] lemma coe_of (V : Type u) [profinitely_filtered_pseudo_normed_group V] : (ProFiltPseuNormGrp.of V : Type u) = V := rfl

@[simp] lemma coe_id (V : ProFiltPseuNormGrp) : ⇑(𝟙 V) = id := rfl

@[simp] lemma coe_comp {A B C : ProFiltPseuNormGrp} (f : A ⟶ B) (g : B ⟶ C) :
  ⇑(f ≫ g) = g ∘ f := rfl

@[simp] lemma coe_comp_apply {A B C : ProFiltPseuNormGrp} (f : A ⟶ B) (g : B ⟶ C) (x : A) :
  (f ≫ g) x = g (f x) := rfl

open pseudo_normed_group

section

variables (M : Type*) [profinitely_filtered_pseudo_normed_group M] (c : ℝ≥0)

instance : t2_space (Top.of (filtration M c)) := by { dsimp, apply_instance }
instance : totally_disconnected_space (Top.of (filtration M c)) := by { dsimp, apply_instance }
instance : compact_space (Top.of (filtration M c)) := by { dsimp, apply_instance }

end

end ProFiltPseuNormGrp

namespace ProFiltPseuNormGrpWithTinv

variables (r' : ℝ≥0)

instance bundled_hom : bundled_hom (@profinitely_filtered_pseudo_normed_group_with_Tinv_hom r') :=
⟨@profinitely_filtered_pseudo_normed_group_with_Tinv_hom.to_fun r',
 @profinitely_filtered_pseudo_normed_group_with_Tinv_hom.id r',
 @profinitely_filtered_pseudo_normed_group_with_Tinv_hom.comp r',
 @profinitely_filtered_pseudo_normed_group_with_Tinv_hom.coe_inj r'⟩

attribute [derive [has_coe_to_sort, large_category, concrete_category]] ProFiltPseuNormGrpWithTinv

/-- Construct a bundled `ProFiltPseuNormGrpWithTinv` from the underlying type and typeclass. -/
def of (r' : ℝ≥0) (M : Type u) [profinitely_filtered_pseudo_normed_group_with_Tinv r' M] :
  ProFiltPseuNormGrpWithTinv r' :=
bundled.of M

instance : has_zero (ProFiltPseuNormGrpWithTinv r') :=
⟨{ α := punit, str := punit.profinitely_filtered_pseudo_normed_group_with_Tinv r' }⟩

instance : inhabited (ProFiltPseuNormGrpWithTinv r') := ⟨0⟩

instance (M : ProFiltPseuNormGrpWithTinv r') :
  profinitely_filtered_pseudo_normed_group_with_Tinv r' M := M.str

@[simp] lemma coe_of (V : Type u) [profinitely_filtered_pseudo_normed_group_with_Tinv r' V] :
  (ProFiltPseuNormGrpWithTinv.of r' V : Type u) = V := rfl

@[simp] lemma of_coe (M : ProFiltPseuNormGrpWithTinv r') : of r' M = M :=
by { cases M, refl }

@[simp] lemma coe_id (V : ProFiltPseuNormGrpWithTinv r') : ⇑(𝟙 V) = id := rfl

@[simp] lemma coe_comp {A B C : ProFiltPseuNormGrpWithTinv r'} (f : A ⟶ B) (g : B ⟶ C) :
  ⇑(f ≫ g) = g ∘ f := rfl

@[simp] lemma coe_comp_apply {A B C : ProFiltPseuNormGrpWithTinv r'} (f : A ⟶ B) (g : B ⟶ C) (x : A) :
  (f ≫ g) x = g (f x) := rfl
open pseudo_normed_group

section

variables (M : Type*) [profinitely_filtered_pseudo_normed_group_with_Tinv r' M] (c : ℝ≥0)
include r'

instance : t2_space (Top.of (filtration M c)) := by { dsimp, apply_instance }
instance : totally_disconnected_space (Top.of (filtration M c)) := by { dsimp, apply_instance }
instance : compact_space (Top.of (filtration M c)) := by { dsimp, apply_instance }

end

-- @[simps] def Filtration (c : ℝ≥0) : ProFiltPseuNormGrp ⥤ Profinite :=
-- { obj := λ M, ⟨Top.of (filtration M c)⟩,
--   map := λ M₁ M₂ f, ⟨f.level c, f.level_continuous c⟩,
--   map_id' := by { intros, ext, refl },
--   map_comp' := by { intros, ext, refl } }


open pseudo_normed_group profinitely_filtered_pseudo_normed_group_with_Tinv_hom

open profinitely_filtered_pseudo_normed_group_with_Tinv (Tinv)

variables {r'}
variables {M M₁ M₂ : ProFiltPseuNormGrpWithTinv.{u} r'}
variables {f : M₁ ⟶ M₂}

/-- The isomorphism induced by a bijective `profinitely_filtered_pseudo_normed_group_with_Tinv_hom`
whose inverse is strict. -/
def iso_of_equiv_of_strict (e : M₁ ≃+ M₂) (he : ∀ x, f x = e x)
  (strict : ∀ ⦃c x⦄, x ∈ filtration M₂ c → e.symm x ∈ filtration M₁ c) :
  M₁ ≅ M₂ :=
{ hom := f,
  inv := inv_of_equiv_of_strict e he strict,
  hom_inv_id' := by { ext x, simp [inv_of_equiv_of_strict, he] },
  inv_hom_id' := by { ext x, simp [inv_of_equiv_of_strict, he] } }

@[simp]
lemma iso_of_equiv_of_strict.apply (e : M₁ ≃+ M₂) (he : ∀ x, f x = e x)
  (strict : ∀ ⦃c x⦄, x ∈ filtration M₂ c → e.symm x ∈ filtration M₁ c) (x : M₁) :
  (iso_of_equiv_of_strict e he strict).hom x = f x := rfl

@[simp]
lemma iso_of_equiv_of_strict_symm.apply (e : M₁ ≃+ M₂) (he : ∀ x, f x = e x)
  (strict : ∀ ⦃c x⦄, x ∈ filtration M₂ c → e.symm x ∈ filtration M₁ c) (x : M₂) :
  (iso_of_equiv_of_strict e he strict).symm.hom x = e.symm x := rfl

def iso_of_equiv_of_strict'
  (e : M₁ ≃+ M₂)
  (strict' : ∀ c x, x ∈ filtration M₁ c ↔ e x ∈ filtration M₂ c)
  (continuous' : ∀ c, continuous (pseudo_normed_group.level e (λ c x, (strict' c x).1) c))
  (map_Tinv' : ∀ x, e (Tinv x) = Tinv (e x)) :
  M₁ ≅ M₂ :=
@iso_of_equiv_of_strict r' M₁ M₂
 {to_fun := e,
  strict' := λ c x, (strict' c x).1,
  continuous' := continuous',
  map_Tinv' := map_Tinv',
  ..e.to_add_monoid_hom } e (λ _, rfl)
  (by { intros c x hx, rwa [strict', e.apply_symm_apply] })

@[simp]
lemma iso_of_equiv_of_strict'_hom_apply
  (e : M₁ ≃+ M₂)
  (strict' : ∀ c x, x ∈ filtration M₁ c ↔ e x ∈ filtration M₂ c)
  (continuous' : ∀ c, continuous (pseudo_normed_group.level e (λ c x, (strict' c x).1) c))
  (map_Tinv' : ∀ x, e (Tinv x) = Tinv (e x))
  (x : M₁) :
  (iso_of_equiv_of_strict' e strict' continuous' map_Tinv').hom x = e x := rfl

@[simp]
lemma iso_of_equiv_of_strict'_inv_apply
  (e : M₁ ≃+ M₂)
  (strict' : ∀ c x, x ∈ filtration M₁ c ↔ e x ∈ filtration M₂ c)
  (continuous' : ∀ c, continuous (pseudo_normed_group.level e (λ c x, (strict' c x).1) c))
  (map_Tinv' : ∀ x, e (Tinv x) = Tinv (e x))
  (x : M₂) :
  (iso_of_equiv_of_strict' e strict' continuous' map_Tinv').inv x = e.symm x := rfl

variables (r')

@[simps]
def Pow (n : ℕ) : ProFiltPseuNormGrpWithTinv.{u} r' ⥤ ProFiltPseuNormGrpWithTinv.{u} r' :=
{ obj := λ M, of r' $ M ^ n,
  map := λ M₁ M₂ f, profinitely_filtered_pseudo_normed_group_with_Tinv.pi_map r' _ _ (λ i, f),
  map_id' := λ M, by { ext, refl },
  map_comp' := by { intros, ext, refl } }

@[simps]
def Pow_Pow_X_equiv (N n : ℕ) :
  M ^ (N * n) ≃+ (M ^ N) ^ n :=
{ to_fun := ((equiv.curry _ _ _).symm.trans (((equiv.prod_comm _ _).trans fin_prod_fin_equiv).arrow_congr (equiv.refl _))).symm,
  map_add' := λ x y, by { ext, refl },
  .. ((equiv.curry _ _ _).symm.trans (((equiv.prod_comm _ _).trans fin_prod_fin_equiv).arrow_congr (equiv.refl _))).symm }

open profinitely_filtered_pseudo_normed_group
open comphaus_filtered_pseudo_normed_group

@[simps]
def Pow_Pow_X (N n : ℕ) (M : ProFiltPseuNormGrpWithTinv.{u} r') :
  (Pow r' N ⋙ Pow r' n).obj M ≅ (Pow r' (N * n)).obj M :=
iso.symm $
iso_of_equiv_of_strict'
  (Pow_Pow_X_equiv r' N n)
  begin
    intros c x,
    dsimp,
    split; intro h,
    { intros i j, exact h (fin_prod_fin_equiv (j, i)) },
    { intro ij,
      have := h (fin_prod_fin_equiv.symm ij).2 (fin_prod_fin_equiv.symm ij).1,
      dsimp at this, simpa only [prod.mk.eta, equiv.apply_symm_apply] using this, },
  end
  begin
    intro c, dsimp,
    rw [← (filtration_pi_homeo (λ _, M ^ N) c).comp_continuous_iff,
        ← (filtration_pi_homeo (λ _, M) c).symm.comp_continuous_iff'],
    apply continuous_pi,
    intro i,
    rw [← (filtration_pi_homeo (λ _, M) c).comp_continuous_iff],
    apply continuous_pi,
    intro j,
    have := @continuous_apply _ (λ _, filtration M c) _ (fin_prod_fin_equiv (j, i)),
    dsimp [function.comp] at this ⊢,
    simpa only [subtype.coe_eta],
  end
  (by { intros, ext, refl })

@[simps hom inv]
def Pow_mul (N n : ℕ) : Pow r' (N * n) ≅ Pow r' N ⋙ Pow r' n :=
nat_iso.of_components (λ M, (Pow_Pow_X r' N n M).symm)
begin
  intros X Y f,
  ext x i j,
  refl,
end

end ProFiltPseuNormGrpWithTinv