category of topological groups

Stream: maths

[Bernd Losert]

I'm noticing that categories like Group and Top are defined using bundled, but this doesn't seem to work when I try to define the category of topological groups. Do I have to define the category by hand?

[Johan Commelin]

Indeed, you can't use bundled to get the category structure, because we don't have the type of continuous group homomorphisms. Only monoid_hom and continuous separately.
We do have docs#group_topology, so you can get halfway there.

The easiest thing to do, might be to define cont_monoid_hom, and then define id and comp for those. Then you can use bundled.

[Bernd Losert]

OK. Let me try.

[Bernd Losert]

Wait a moment. one_hom and mul_hom both have a to_fun. When I combine these, does that mean I will have two to_fun functions and I will have to add continuous one_hom.to_fun and continuous mul_hom.to_fun?

[Johan Commelin]

@Bernd Losert They have already been combined into docs#monoid_hom . So I don't think you should need to combine them again yourself.

[Bernd Losert]

But how does monoid_hom fix the problem with the two to_fun functions?

[Yaël Dillies]

This is the point of extending structures. monoid_hom only has one to_fun, which is used for both properties.

[Bernd Losert]

import tactic
import topology.algebra.group
import category_theory.concrete_category.bundled
import algebra.group.hom

open category_theory

universe u

structure cont_monoid_hom (M N : Type*) [mul_one_class M] [mul_one_class N] extends monoid_hom M N :=
(to_fun_continuous : continuous to_fun)

does not work for me.

[Yaël Dillies]

You're missing a topology on M and N.

[Bernd Losert]

Doh!

[Bernd Losert]

I get this now:

error: invalid 'structure' header, field 'to_fun' from 'mul_hom' has already been declared

[Yaël Dillies]

Weird... run_cmd old_structures true before should solve it, but that's unsatisfactory as this use is getting phased out.

[Bernd Losert]

That did not work either:

import tactic
import topology.algebra.group
import category_theory.concrete_category.bundled
import algebra.group.hom

open category_theory

universe u

run_cmd old_structures true

structure cont_monoid_hom (M N : Type*) [mul_one_class M] [mul_one_class N] [topological_space M] [topological_space N] extends one_hom M N, mul_hom M N :=
(to_fun_continuous : continuous to_fun)

gives

/Users/bernd/Repositories/convergence/src/test.lean:10:8: error: unknown identifier 'old_structures'
/Users/bernd/Repositories/convergence/src/test.lean:10:0: error: don't know how to synthesize placeholder
context:
⊢ Type
/Users/bernd/Repositories/convergence/src/test.lean:12:141: error: invalid 'structure' header, field 'to_fun' from 'mul_hom' has already been declared

[Yakov Pechersky]

set_option old_structure_cmd true

[Yaël Dillies]

Ah thanks

[Bernd Losert]

Is there a tutorial about how to use bundled? I'm still confused. And if I decide not to use bundled, how would I define the category of topological groups? Should I make a TopGroup structure containing group, topological_space, topological_group fields?

[Bernd Losert]

I was hoping I could just write def TopGroup := Σ (α : Type u), topological_group α, but that doesn't work.

[Johan Commelin]

I think you can use docs#group_topology

[Johan Commelin]

There is no tutorial on how to use bundled. I guess the only way is to look at (i) its implementation and (ii) examples of how it's used in mathlib such as docs#Top and docs#Ab.

[Bernd Losert]

Do you happen to know of an example where the category had to be built without using bundled?

[Bernd Losert]

In particular, a category like that of topological groups where you have to mix things from two separate domains.

[Johan Commelin]

There is docs#Module

[Johan Commelin]

If you want a long list of categories, look at docs#category_theory.category and click on the dropdown "▸ Instances"

[Bernd Losert]

Nice. I started doing something similar for TopGroup. I'll have to repeat this process when I define the category of continuous group actions.

[Johan Commelin]

Out of curiousity: what is your end goal?

[Bernd Losert]

I'm formalizing some of my research on convergence spaces (a generalization of top. spaces).

[Johan Commelin]

I see. Is there a 2-line explanation how TopGroup (and the category of continuous group actions) show up when working with convergence spaces?

[Johan Commelin]

I remember your other thread about setting up convergence spaces. And I just learned from wiki that the category of convergence spaces has exponentials. Is this one of the results you are aiming at as preliminary?

[Bernd Losert]

Yep, the category of convergence spaces has exponentionals, which is one of the reasons it's better than Top.

[Johan Commelin]

Right. So where does TopGroup fit into this picture?

[Bernd Losert]

I don't particularly care about TopGroup. I'm just using it as an example.

[Johan Commelin]

Aha.

[Bernd Losert]

What I actually care about is ConvGroup.

[Johan Commelin]

Btw, the category of condensed sets also has exponentials

[Johan Commelin]

Is ConvAb an abelian category?

[Bernd Losert]

No, it's not Abelian unfortunately.

[Johan Commelin]

Would be interesting to know if the functor Conv → Cond(Set) is well behaved.

[Bernd Losert]

Yes. That would be something to look at. At the moment, my advisor and I are generalizing the theory of continuous partial group actions on topological spaces to the convergence space setting.

[Bernd Losert]

So I have the following:

import topology.algebra.group
import category_theory.concrete_category.bundled
import algebra.group.hom
import topology.category.Top

open category_theory

universe u

set_option old_structure_cmd true

structure TopGroup :=
(carrier : Type*)
(the_group : group carrier)
(the_topological_space : topological_space carrier)
(the_topological_group : topological_group carrier)

namespace TopGroup

structure hom (G H : TopGroup) :=
(to_fun : G.carrier → H.carrier)
(to_fun_continuous : continuous to_fun)
(to_fun_group_hom : monoid_hom G.carrier H.carrier to_fun)

end TopGroup

Unfortunately Lean complains:

error: invalid field notation, 'to_mul_one_class' is not a valid "field" because environment does not contain 'group.to_mul_one_class'
  G.is_group
which has type
  group G.carrier

I'm not sure how to fix this. Passing the group instances manually to monoid_hom does not seem to work either. (I was hoping it would do some coercion magic.)

[Adam Topaz]

You need to define the instances as instances for monoid_hom to work. Take a look, for example, at the definitions around docs#Group

[Alex J. Best]

E.g

import topology.algebra.group
import category_theory.concrete_category.bundled
import algebra.group.hom
import topology.category.Top
import deprecated.group

open category_theory

universe u

--set_option old_structure_cmd true

structure TopGroup :=
(carrier : Type*)
(the_group : group carrier)
(the_topological_space : topological_space carrier)
(the_topological_group : topological_group carrier)


instance (G : TopGroup) : group G.carrier := G.the_group
instance (G : TopGroup) : topological_space G.carrier := G.the_topological_space
namespace TopGroup

structure hom (G H : TopGroup) :=
(to_fun : G.carrier → H.carrier)
(to_fun_continuous : continuous to_fun)
(to_fun_group_hom : is_monoid_hom to_fun)

[Alex J. Best]

I had to import deprecated.group to get access to is_monoid_hom as monoid_hom is the bundled type

[Adam Topaz]

Presumably hom should extend monoid_hom

[Alex J. Best]

Also you may want to copy Group more closely and define a coe_to_sort for TopGroup so you don't need to add .carrier everywhere

[Bernd Losert]

Cool. Thank you.

[Scott Morrison]

Sorry I'm late to this thread, but I don't think TopCommRing has been mentioned yet, which is I think the example you are looking for.