Zulip Chat Archive

Stream: condensed mathematics

Topic: def of comphaus_filtered_pseudo_normed_group_hom


Kevin Buzzard (Mar 31 2022 at 11:41):

I'm feeling my way back into LTE. The definition of comphaus_filtered_pseudo_normed_group_hom (in pseudo_normed_group/profinitely_filtered.lean) is supposed to capture the concept of a morphism of comphaus_filtered_pseudo_normed_groups. My memory was that Peter was reluctant to put a topology on the full underlying abelian group (although there are topologies on the filtrands), and right now the definition of a morphism f:M->N between two such things has to be "continuous" in the sense that if f happens to map the filtrand M_c into N_d then this induced map between topological spaces has to be continuous.

OK so can the following happen: M is a comphaus_filtered_pseudo_normed_group and M=M_1=M_2 (this is the filtration), but the topologies on M_1 and M_2 are distinct, the inclusion from M_1 to M_2 is continuous, but the inclusion from M_2 to M_1 is not. If that's allowed then according to current definitions, the identity function is not continuous, because it happens to map M_2 into M_1 but this map isn't continuous. Is that OK?

Kevin Buzzard (Mar 31 2022 at 11:57):

This could be fixed by changing

(continuous' :  c₁ c₂ (f₀ : filtration M₁ c₁  filtration M₂ c₂)
  (h :  x, to_fun x = f₀ x), continuous f₀)

to the weaker condition that there exists some c3>=c2 such that the induced map M₁ c₁ → M₂ c3 is continuous.

Kevin Buzzard (Mar 31 2022 at 12:08):

Oh wait I must be wrong because I've just run into the definition of id :-/

Kevin Buzzard (Mar 31 2022 at 12:12):

Aah, got it: all the filtrands are compact and Hausdorff so continuous bijections are necessarily homeomorphisms. OK I am no longer confused :-)

Johan Commelin (Mar 31 2022 at 13:21):

Note that in all concrete situations, those topologies are either discrete, or they should come with a lemma called continuous_iff that should give you a workable goal after rewriting with it.


Last updated: Dec 20 2023 at 11:08 UTC