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_group
s. 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