defining the category ConvGroup

Stream: maths

[Bernd Losert]

So, I have this code:

import tactic
import category_theory.concrete_category.bundled
import algebra.group.hom
import deprecated.group
import order.filter.partial
import algebra.support

noncomputable theory
open set function filter classical option category_theory
open_locale classical filter

universe u

variables {X Y Z : Type*}

set_option old_structure_cmd true

structure convergence_space (X : Type*) :=
(converges : filter X → X → Prop)
(pure_converges : ∀ x, converges (pure x) x)
(le_converges : ∀ {ℱ 𝒢}, ℱ ≤ 𝒢 → ∀ {x}, converges 𝒢 x → converges ℱ x) -- ℱ ≤ 𝒢 means 𝒢 ⊆ ℱ

attribute [ext] convergence_space
attribute [class] convergence_space

open convergence_space

def continuous [p : convergence_space X] [q : convergence_space Y] (f : X → Y) : Prop :=
∀ {x} {ℱ}, p.converges ℱ x → q.converges (map f ℱ) (f x)

lemma continuous.comp
[p : convergence_space X] [q : convergence_space Y] [r : convergence_space Z] {g : Y → Z} {f : X → Y}
(hg : continuous g) (hf : continuous f) : continuous (g ∘ f) := begin
  assume x : X,
  assume ℱ : filter X,
  assume : p.converges ℱ x,
  have : q.converges (map f ℱ) (f x), from hf this,
  have : r.converges (map g (map f ℱ)) (g (f x)), from hg this,
  convert this,
end

instance [p : convergence_space X] [q : convergence_space Y] : convergence_space (X × Y) := sorry

class has_continuous_mul (X : Type*) [convergence_space X] [has_mul X] : Prop :=
(continuous_mul : continuous (λ p : X × X, p.1 * p.2))

class convergence_group (G : Type*) [convergence_space G] [group G] extends has_continuous_mul G : Prop :=
(continuous_inv : continuous (has_inv.inv : G → G))

structure ConvGroup :=
(carrier : Type*)
[is_group : group carrier]
[is_convergence_space : convergence_space carrier]
[is_convergence_group : convergence_group carrier]

instance (G : ConvGroup) : group G.carrier := G.is_group
instance (G : ConvGroup) : convergence_space G.carrier := G.is_convergence_space
instance : has_coe_to_sort ConvGroup Type* := ⟨ConvGroup.carrier⟩

namespace ConvGroup

structure hom (G H : ConvGroup) :=
(to_fun : G → H)
(to_fun_continuous : continuous to_fun)
(to_fun_group_hom : is_monoid_hom to_fun)

instance (G H : ConvGroup) : has_coe_to_fun (hom G H) (λ _, G → H) := ⟨hom.to_fun⟩

end ConvGroup

instance : category ConvGroup := {
  hom := ConvGroup.hom,
  comp := λ G H K f g, {
    to_fun := g ∘ f,
    to_fun_continuous := begin
      exact continuous.comp (g.to_fun_continuous) (f.to_fun_continuous), -- THIS IS WHERE I AM STUCK
    end,
    to_fun_group_hom := sorry,
  },
  id := λ G, {
    to_fun := λ x, x,
    to_fun_continuous := sorry,
    to_fun_group_hom := sorry,
  },
}

I get some error about an invalid type ascription, which is weird because I am not using any in the proof. I don't know what to do here. Help!

[Kevin Buzzard]

Can you post the error?

[Bernd Losert]

/Users/bernd/Repositories/convergence/src/test.lean:42:0: warning: declaration 'prod.convergence_space' uses sorry
/Users/bernd/Repositories/convergence/src/test.lean:79:12: error: invalid type ascription, term has type
  (ConvGroup.carrier.convergence_space G).converges ?m_1 ?m_2 →
  (ConvGroup.carrier.convergence_space K).converges (map (g.to_fun ∘ f.to_fun) ?m_1) ((g.to_fun ∘ f.to_fun) ?m_2)
but is expected to have type
  continuous (⇑g ∘ ⇑f)
state:
G H K : ConvGroup,
f : G ⟶ H,
g : H ⟶ K
⊢ continuous (⇑g ∘ ⇑f)

[David Wärn]

The problem is with the brackets in your definition of continuous. Change it to ∀ ⦃x ℱ⦄.

[Bernd Losert]

Oh wow. This is my first time running into this kind of problem. I forgot what ⦃ ⦄ are used for.

[Bernd Losert]

OK, I found an explanation here: https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html#more-on-implicit-arguments. However, I'm still confused why it fixes my issue.

[Patrick Massot]

I would say this ⦃ ⦄ trick is an accidental workaround. This is an elaborator bug, your code should work (and you can make it work it you use @ to help. Your definition of continuity is known to bring elaboration issues. That's why continuous is a structure in mathlib. You can use the following code:

import tactic
import category_theory.concrete_category.bundled
import algebra.group.hom
import deprecated.group
import order.filter.partial
import algebra.support

noncomputable theory
open set function filter classical option category_theory
open_locale classical filter

universe u

variables {X Y Z : Type*}

set_option old_structure_cmd true

@[ext] class convergence_space (X : Type*) :=
(converges : filter X → X → Prop)
(pure_converges : ∀ x, converges (pure x) x)
(le_converges : ∀ {ℱ 𝒢}, ℱ ≤ 𝒢 → ∀ {x}, converges 𝒢 x → converges ℱ x) -- ℱ ≤ 𝒢 means 𝒢 ⊆ ℱ


open convergence_space


structure continuous [convergence_space X] [convergence_space Y] (f : X → Y) : Prop :=
(cvg : ∀ {x} {ℱ}, converges ℱ x → converges (map f ℱ) (f x))

lemma continuous.comp [convergence_space X] [convergence_space Y] [convergence_space Z]
  {g : Y → Z} {f : X → Y} (hg : continuous g) (hf : continuous f) : continuous (g ∘ f) :=
⟨λ x ℱ h, hg.cvg (hf.cvg h)⟩


instance [convergence_space X] [convergence_space Y] : convergence_space (X × Y) := sorry

class has_continuous_mul (X : Type*) [convergence_space X] [has_mul X] : Prop :=
(continuous_mul : continuous (λ p : X × X, p.1 * p.2))

class has_continuous_smul (S X : Type*) [has_scalar S X] [convergence_space S] [convergence_space X] : Prop :=
(continuous_smul : continuous (λ p : S × X, p.1 • p.2))

class convergence_group (G : Type*) [convergence_space G] [group G] extends has_continuous_mul G : Prop :=
(continuous_inv : continuous (has_inv.inv : G → G))

structure ConvGroup :=
(carrier : Type*)
[is_group : group carrier]
[is_convergence_space : convergence_space carrier]
[is_convergence_group : convergence_group carrier]

instance (G : ConvGroup) : group G.carrier := G.is_group
instance (G : ConvGroup) : convergence_space G.carrier := G.is_convergence_space
instance : has_coe_to_sort ConvGroup Type* := ⟨ConvGroup.carrier⟩

namespace ConvGroup

structure hom (G H : ConvGroup) :=
(to_fun : G → H)
(to_fun_continuous : continuous to_fun)
(to_fun_group_hom : is_monoid_hom to_fun)

instance (G H : ConvGroup) : has_coe_to_fun (hom G H) (λ _, G → H) := ⟨hom.to_fun⟩

lemma hom.continuous {G H : ConvGroup} (f : hom G H) : continuous f := f.to_fun_continuous

def hom.comp {G H K : ConvGroup} (g : hom H K) (f : hom G H) : hom G K :=
{ to_fun := g ∘ f,
  to_fun_continuous := g.continuous.comp f.continuous,
  to_fun_group_hom := f.to_fun_group_hom.comp g.to_fun_group_hom }

end ConvGroup

instance : category ConvGroup := {
  hom := ConvGroup.hom,
  comp := λ G H K f g, g.comp f,
  id := λ G, {
    to_fun := λ x, x,
    to_fun_continuous := sorry,
    to_fun_group_hom := sorry,
  },
}

[Patrick Massot]

Note that I also removed all your instance variable names. If you really want this to be a class then you should very rarely need to name instance inputs.

[Bernd Losert]

Ah, I was wondering why continuous was a structure in instead of a plain Prop. So what is the general advice here? Use a structure or use these weak implicit arguments?