Zulip Chat Archive

Stream: maths

Topic: separated quotient


view this post on Zulip Patrick Massot (Sep 30 2018 at 20:18):

@Johannes Hölzl why https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/completion.lean#L185 is not an instance?

view this post on Zulip Patrick Massot (Sep 30 2018 at 20:19):

Oh! Why this completeness assumption?!

view this post on Zulip Patrick Massot (Sep 30 2018 at 20:20):

I love doing that with Lean: I removed the assumption and the proof still compiles!

view this post on Zulip Johannes Hölzl (Sep 30 2018 at 20:39):

yeah should be instance

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 20:44):

Yeah for removing assumptions. You remove them in real life and then have to understand the proof all over again

view this post on Zulip Patrick Massot (Sep 30 2018 at 20:44):

exactly

view this post on Zulip Patrick Massot (Sep 30 2018 at 20:58):

I just noticed while reviewing my work that this unneeded assumption is simply copy-paste from the previous lemma (where it is needed).

view this post on Zulip Patrick Massot (Sep 30 2018 at 21:01):

Anyway, @Johannes Hölzl please have a look at https://github.com/leanprover-community/mathlib/commit/cfb60c52739921a0a9b36bbe2a73400dc2fc372a

view this post on Zulip Patrick Massot (Sep 30 2018 at 21:02):

The nonempty quotient stuff will have to move to its proper place but I don't have courage right now (it means recompiling all mathlib since the proper place is very low in the tree).

view this post on Zulip Patrick Massot (Sep 30 2018 at 21:03):

Kevin: this commit is still work towards ring completions. It's preparation for the isomorphism from completion (separation_quotient a) to completion a.

view this post on Zulip Patrick Massot (Sep 30 2018 at 21:05):

We're getting really close. We may have ring completion tomorrow if I can hide from my secretary and from the head of my department. But first I need to sleep.

view this post on Zulip Patrick Massot (Oct 01 2018 at 07:08):

@Johannes Hölzl I just noticed that some lemmas from my versions of uniform spaces completions didn't make it through your refactoring. In particular https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/completions/src/for_mathlib/completion.lean#L266-L267 and https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/completions/src/for_mathlib/completion.lean#L274 (I realized I forgot the analogue of the last one for the separation quotient yesterday). Is it on purpose? From a categorical point of view they are crucial.

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 07:40):

sorry, both got lost. I will add them

view this post on Zulip Patrick Massot (Oct 01 2018 at 08:36):

It's ok, I can add them back

view this post on Zulip Patrick Massot (Oct 01 2018 at 08:44):

Just to make sure: Johannes, are you working on this?

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 08:47):

Not yet, I wanted to start now. Do you have some changes?

view this post on Zulip Patrick Massot (Oct 01 2018 at 08:48):

No, I was about to start :smile:

view this post on Zulip Patrick Massot (Oct 01 2018 at 08:48):

I'll let you do this, and work on the next steps

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 08:48):

okay

view this post on Zulip Patrick Massot (Oct 01 2018 at 08:49):

Did you pull what I did yesterday?

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 08:49):

One thing I will also change: remove is_ideal'. I don't think it is necessary.

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 08:49):

yes, i just pulled

view this post on Zulip Patrick Massot (Oct 01 2018 at 08:49):

Fine. I was worried that nobody reacted to this is_ideal'

view this post on Zulip Patrick Massot (Oct 01 2018 at 08:50):

But I hope the topology proof won't become ugly

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 08:52):

I hope so, too. That's why I plan to remove it again. If it gets ugly I will add a "constructor" function for is_ideal instead of the additional structure

view this post on Zulip Patrick Massot (Oct 01 2018 at 08:52):

Ok, great. I'll stop asking questions and let you work then

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 11:27):

So I restructured a little bit and replaced the proof for is_ideal (closure _), by adding nicer rules for membership in closure.

view this post on Zulip Patrick Massot (Oct 01 2018 at 11:28):

I see you pushed while I was writing a link to the previous version :)

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 11:30):

Hehe good. I guess you want to work now on the ring completion without assuming Hausdorff?

view this post on Zulip Patrick Massot (Oct 01 2018 at 11:31):

Yes, and then you'll have the pleasure to refactor it

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 11:32):

No problem. I'm sure it will be in a good state!

view this post on Zulip Patrick Massot (Oct 01 2018 at 11:33):

I'm a bit sad that the proof of ideal_closure is no unrecognizable for mathematicians

view this post on Zulip Patrick Massot (Oct 01 2018 at 11:33):

I don't know why you and Mario don't like equalities between functions.

view this post on Zulip Patrick Massot (Oct 01 2018 at 11:34):

It's really going against main stream mathematics to replace function equality with elements equality everywhere

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 11:34):

No I'm confused. I think it is much more readable than before. We state what kind of steps we proof (is it the zero, add, or mul case) and we say how we proof the membership in the closure. Before it was just a sequence of tactics, not mentioning which case is proved.

view this post on Zulip Patrick Massot (Oct 01 2018 at 11:35):

Category theory tells us that elements are confusing, only arrows matter

view this post on Zulip Patrick Massot (Oct 01 2018 at 11:36):

I agree that stating which case we are proving is nice. What I'm talking about is hiding that the proof key is image_closure_subset_closure_image

view this post on Zulip Patrick Massot (Oct 01 2018 at 11:36):

that you've hidden in mem_closure

view this post on Zulip Patrick Massot (Oct 01 2018 at 11:37):

also that name is much harder to find than image_closure_subset_closure_image

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 12:07):

why is it harder to find? You ask, "is there anything to prove membership in closure" then you find it. if you ask: is there anything w.r.t. subset of closure you don't find it. But both are valid. Your proof might be more categorical. But only halfway, you proof something about subsets, not about arrows. You still use closure_mono, instead of arguing about an mono-homomorphism into another type.

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 12:08):

closure is very set based, so for me it doesn't make sense to argue about arrows.

view this post on Zulip Patrick Massot (Oct 01 2018 at 13:37):

No problem. I'm sure it will be in a good state!

@Johannes Hölzl it's your turn: https://github.com/leanprover-community/mathlib/commit/b0592fe97e74ef4e9af8158052d30053914d639b

view this post on Zulip Patrick Massot (Oct 01 2018 at 13:37):

I'm sure you'll find better names :wink:

view this post on Zulip Kevin Buzzard (Oct 01 2018 at 14:45):

I find these conversations very interesting. Patrick is absolutely right from a mathematical point of view. Grothendieck stressed that the arrows were more important than the objects. People talked about geometric objects being smooth but Grothendieck argued that the correct definition was that of a map being smooth, and an object being smooth just meant that the map from this object to the one point set was smooth. On the other hand Johannes thinks about mathematics in a completely different way. Do people properly understand how Grothendieck's ideas should influence type theory?

view this post on Zulip Patrick Massot (Oct 01 2018 at 19:02):

Hum, I built a ring structure on the separation quotient of a topological ring, but forgot to prove that it's a topological ring

view this post on Zulip Patrick Massot (Oct 01 2018 at 19:02):

I'll need that projection on a quotient group is open

view this post on Zulip Patrick Massot (Oct 01 2018 at 19:03):

Do we have open maps in mathlib?

view this post on Zulip Reid Barton (Oct 01 2018 at 19:05):

Don't think so, there's embedding_open I think which says that an embedding of an open subspace is an open map, but just spelled out explicitly.

view this post on Zulip Patrick Massot (Oct 01 2018 at 19:06):

I'm not sure how to get back the fact that addition on a group quotient group is defined by quotient.lift. Should I dunfold until I see it or is there a better way?

view this post on Zulip Chris Hughes (Oct 01 2018 at 19:24):

use show

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 19:26):

dsimp could also help.

view this post on Zulip Patrick Massot (Oct 01 2018 at 19:31):

I'm completely lost in our maze of quotient structures. Do we have the quotient of a commutative additive group by a subgroup? Is it related in anyway with quotient rings? Or should I be doing topological modules?

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 19:35):

quotient_add_group.add_group (https://github.com/leanprover/mathlib/blob/master/group_theory/quotient_group.lean#L46)
is for normal subgroups, but as far as I understand a normal subgroup is just a subgroup in the commutative case?

view this post on Zulip Patrick Massot (Oct 01 2018 at 19:35):

yes, every group is normal in this case

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 19:38):

so you can use quotient_add_group?

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 19:39):

Ah there is also quotient_add_group.add_comm_group it is just not setup as an instance

view this post on Zulip Patrick Massot (Oct 01 2018 at 19:40):

What about https://github.com/leanprover/mathlib/blob/master/group_theory/quotient_group.lean#L53?

view this post on Zulip Patrick Massot (Oct 01 2018 at 19:41):

It looks good but I haven't managed to use it yet

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 19:46):

Yes, that's it, but the multiplicative version. Afterwards the additive version is derived (line 63). But for the additive version the instance attribute is missing

view this post on Zulip Patrick Massot (Oct 01 2018 at 19:46):

Oh

view this post on Zulip Patrick Massot (Oct 01 2018 at 19:52):

Now it seems to work without the attribute, strange...

view this post on Zulip Johannes Hölzl (Oct 01 2018 at 19:57):

maybe its somewhere else?

view this post on Zulip Patrick Massot (Oct 01 2018 at 20:00):

I need to stop for today, but at least I have some statement:

import analysis.topology.topological_structures

variables {α : Type*} [add_comm_group α] [topological_space α]

instance [topological_add_group α] (N : set α) [is_add_subgroup N]: topological_space (quotient_add_group.quotient N) :=
by dunfold quotient_add_group.quotient ; apply_instance

instance [topological_add_group α] (N : set α) [is_add_subgroup N]: topological_add_group (quotient_add_group.quotient N) :=
{ continuous_add := sorry,
  continuous_neg := sorry}

view this post on Zulip Patrick Massot (Oct 01 2018 at 20:01):

I wasn't able to get to the point where I can simply use continuity of lifts of continuous functions

view this post on Zulip Johannes Hölzl (Oct 02 2018 at 07:53):

@Patrick Massot fyi, I rebased the branch. So pull the new branch before continuing on it.

view this post on Zulip Patrick Massot (Oct 03 2018 at 16:08):

I tried to return to this topological quotient group, but I still have no idea how to unfold the definition of addition on the quotient. It uses a mysterious quotient.lift_on2' that I can't reach, even using change. The MWE is:

import analysis.topology.topological_structures
import group_theory.quotient_group

variables {α : Type*} [add_comm_group α] [topological_space α]
  [topological_add_group α] (N : set α) [is_add_subgroup N]

instance [topological_add_group α] (N : set α) [is_add_subgroup N]: topological_space (quotient_add_group.quotient N) :=
by dunfold quotient_add_group.quotient ; apply_instance

instance : topological_add_group (quotient_add_group.quotient N) :=
{ continuous_add := sorry,
  continuous_neg := sorry}

view this post on Zulip Johan Commelin (Oct 03 2018 at 16:23):

@Patrick Massot Do you have a strategy in mind?

view this post on Zulip Johan Commelin (Oct 03 2018 at 16:23):

Which ingredients would you want to apply?

view this post on Zulip Johan Commelin (Oct 03 2018 at 16:25):

My guess would be that you first need to turn the addition into a map quot × quot → quot, then identify quot × quot with an appropriate quotient. And then apply some lemma about the universal property of quotients and continuous maps

view this post on Zulip Johan Commelin (Oct 03 2018 at 16:25):

Of course this is very vague...

view this post on Zulip Johannes Hölzl (Oct 03 2018 at 16:36):

So, quotient.lift_on2' is just quotient.lift_on2 using a implicit parameter instead of a type class parameter. If this helps...

view this post on Zulip Reid Barton (Oct 03 2018 at 17:22):

I think the math strategy is to start with a commutative square involving the multiplication G×GGG \times G \to G and the multiplication G/H×G/HG/HG/H \times G/H \to G/H. Right?

view this post on Zulip Reid Barton (Oct 03 2018 at 17:24):

Where the vertical maps are q×qq \times q and qq where q:GG/Hq : G \to G/H is the quotient map. I think the fact that that square commutes is a definitional equality (for each pair (g1,g2)G×G(g_1, g_2) \in G \times G). So you should not have to unfold the definition of the product in G/HG/H if that is correct.

view this post on Zulip Chris Hughes (Oct 03 2018 at 17:27):

@Patrick Massot the fact that quotient_group.mk is a group_hom should mean that you don't need to unfold mul. The proof that it is a group_hom is just rfl anyway, so everything's definitionally equal to what you want it to be.

view this post on Zulip Reid Barton (Oct 03 2018 at 17:31):

The point is that the multiplication on the quotient is ultimately defined in terms of quot.lift, and quot.lift applied to something made from quot.mk reduces.

view this post on Zulip Johan Commelin (Oct 03 2018 at 17:36):

Ok, so first of all we need to know that the quotient map is ctu. Is this already there?

view this post on Zulip Reid Barton (Oct 03 2018 at 17:43):

Assuming "ctu" = continuous then continuous_quot_mk

view this post on Zulip Reid Barton (Oct 03 2018 at 17:46):

By the way, this one is not simply a formal consequence of the universal property of the quotient, because the product of two quotient maps is not in general a quotient map (although in this case I guess it probably is)

view this post on Zulip Reid Barton (Oct 03 2018 at 17:46):

For continuous_neg, you can argue along those lines.

view this post on Zulip Patrick Massot (Oct 03 2018 at 18:41):

Sorry, I was away. Indeed the quotient projection is continuous, and addition is continuous, so I want to use https://github.com/leanprover/mathlib/blob/c1f9f2e2977c0f6cb1cfd949bee8c3817cce0489/analysis/topology/continuity.lean#L811 applied to quotient.mk \circ addition. My problem is to get Lean to swallow that

view this post on Zulip Patrick Massot (Oct 03 2018 at 18:47):

oh maybe I misunderstood. Do you mean I could use https://github.com/leanprover/mathlib/blob/c1f9f2e2977c0f6cb1cfd949bee8c3817cce0489/analysis/topology/continuity.lean#L383?

view this post on Zulip Patrick Massot (Oct 03 2018 at 18:48):

lemma quotient_map.continuous_iff {f : α → β} {g : β → γ} (hf : quotient_map f) : continuous g ↔ continuous (g ∘ f)

view this post on Zulip Patrick Massot (Oct 03 2018 at 18:50):

I'm waiting for mathlib to compile...

view this post on Zulip Chris Hughes (Oct 03 2018 at 18:55):

Is continuous_quot_mk the right quot_mk? I see no mention of groups anywhere around it

view this post on Zulip Patrick Massot (Oct 03 2018 at 18:55):

The topology on the quotient group is the quotient topology (I hope)

view this post on Zulip Reid Barton (Oct 03 2018 at 19:21):

You can't use continuous_quotient_lift or quotient_map.continuous_iff because G/H×G/HG/H \times G/H is not (obviously) a quotient of G×GG \times G

view this post on Zulip Reid Barton (Oct 03 2018 at 19:23):

I thought you were doing the proof which goes like: qq is an open map (because q1(q(U))q^{-1}(q(U)) is a union of translates of UU, hence open), so q×qq \times q is an open map, and then you can check that the preimage of an open subset of G/HG/H under multiplication is again open by chasing around the square

view this post on Zulip Patrick Massot (Oct 03 2018 at 19:25):

Indeed this is what I wanted to do the other day (I even asked whether we have a definition of open maps in mathlib) and then I forgot what I was doing...

view this post on Zulip Patrick Massot (Oct 03 2018 at 19:26):

But I guess the map from G×GG \times G to G/H×G/HG/H \times G/H should still be a quotient map

view this post on Zulip Patrick Massot (Oct 03 2018 at 19:27):

I need to think on paper

view this post on Zulip Patrick Massot (Oct 03 2018 at 19:53):

I decided that every proof will need to first prove that GG/HG \to G/H is open anyway.

view this post on Zulip Kenny Lau (Oct 03 2018 at 19:55):

why do I feel like I've proved that

view this post on Zulip Patrick Massot (Oct 03 2018 at 19:55):

I'd be very interested

view this post on Zulip Patrick Massot (Oct 03 2018 at 19:55):

Do you remember if this is in mathlib?

view this post on Zulip Kenny Lau (Oct 03 2018 at 19:59):

def topological_group.coinduced {α : Type u} {β : Type v}
  [t : topological_group α] [group β]
  (f : α  β) [is_group_hom f] (hf1 : function.surjective f)
  (hf2 :  S, is_open S  is_open (f ⁻¹' (f '' S))) :
  topological_group β :=

hf2 seems to say that it is an open map

view this post on Zulip Kenny Lau (Oct 03 2018 at 19:59):

instance quotient_group.topological_group (G : Type u)
  [topological_group G] (N : set G) [normal_subgroup N] :
  topological_group (left_cosets N) :=
by letI := left_rel N; from
topological_group.coinduced quotient.mk quotient.exists_rep (λ S hs,
have ( x : {x // x = 1}, (λ y, x.1 * y) ⁻¹' S)
    = quotient.mk ⁻¹' (quotient.mk '' S),
  from set.ext $ λ z,
  ⟨λ S, ⟨⟨g, h1, rfl, h2, g * z, h2,
    by rw [is_group_hom.mul quotient.mk, h1, one_mul];
    from quotient_group.is_group_hom _⟩,
  λ g, h1, h2, ⟨_, ⟨⟨g * z⁻¹,
    by rw [is_group_hom.mul quotient.mk, h2, is_group_hom.inv quotient.mk, mul_inv_self];
    repeat { from quotient_group.is_group_hom _ }, rfl,
    by simp [h1]⟩⟩,
this  is_open_Union $ λ x : {x // x = 1},
continuous_mul continuous_const continuous_id _ hs)

so this consistutes a proof

view this post on Zulip Kenny Lau (Oct 03 2018 at 20:00):

https://github.com/kckennylau/local-langlands-abelian/blob/master/src/topological_group.lean#L205-L221

view this post on Zulip Kenny Lau (Oct 03 2018 at 20:01):

@Patrick Massot is this what you want?

view this post on Zulip Patrick Massot (Oct 03 2018 at 20:01):

it looks very much like what I want

view this post on Zulip Kenny Lau (Oct 03 2018 at 20:02):

nice

view this post on Zulip Patrick Massot (Oct 03 2018 at 20:02):

I mean the statement of course

view this post on Zulip Kenny Lau (Oct 03 2018 at 20:02):

I mean, it's not hard to prove

view this post on Zulip Patrick Massot (Oct 03 2018 at 20:02):

the proof...

view this post on Zulip Kenny Lau (Oct 03 2018 at 20:03):

a first year could learn that

view this post on Zulip Patrick Massot (Oct 03 2018 at 20:03):

the math proof is easy yes

view this post on Zulip Patrick Massot (Oct 03 2018 at 20:04):

reading a term mode proof is hard (for me)

view this post on Zulip Kenny Lau (Oct 03 2018 at 20:04):

this proof is 3 months old btw

view this post on Zulip Patrick Massot (Oct 03 2018 at 20:06):

I will need to redo it in my context and state intermediate lemmas for reuse anyway

view this post on Zulip Patrick Massot (Oct 03 2018 at 20:06):

but it's still helpful to have one full proof

view this post on Zulip Kenny Lau (Oct 03 2018 at 20:07):

ok

view this post on Zulip Patrick Massot (Oct 03 2018 at 20:08):

thanks!

view this post on Zulip Patrick Massot (Oct 03 2018 at 20:11):

Did you think about PRing stuff from this repo?

view this post on Zulip Kenny Lau (Oct 03 2018 at 20:11):

maybe

view this post on Zulip Patrick Massot (Oct 03 2018 at 20:20):

Remember your work is lost if you don't PR it

view this post on Zulip Kevin Buzzard (Oct 04 2018 at 06:40):

The first key thing we need from Kenny's repo is algebraic closure, and it's not in there yet. Kenny is waiting for module refactoring because the argument needs loads of ideals over loads of rings.

view this post on Zulip Kevin Buzzard (Oct 04 2018 at 06:41):

After that we need to take a level-headed look at how much is appropriate for mathlib and how much really just a wacky independent project

view this post on Zulip Kevin Buzzard (Oct 04 2018 at 06:41):

(and I don't know what the conclusion will be)


Last updated: May 12 2021 at 08:14 UTC