Zulip Chat Archive

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).

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.

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.

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.

Johannes Hölzl (Oct 01 2018 at 07:40):

sorry, both got lost. I will add them

Patrick Massot (Oct 01 2018 at 08:36):

It's ok, I can add them back

Patrick Massot (Oct 01 2018 at 08:44):

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

Johannes Hölzl (Oct 01 2018 at 08:47):

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

Patrick Massot (Oct 01 2018 at 08:48):

No, I was about to start :smile:

Patrick Massot (Oct 01 2018 at 08:48):

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

Johannes Hölzl (Oct 01 2018 at 08:48):

okay

Patrick Massot (Oct 01 2018 at 08:49):

Did you pull what I did yesterday?

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.

Johannes Hölzl (Oct 01 2018 at 08:49):

yes, i just pulled

Patrick Massot (Oct 01 2018 at 08:49):

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

Patrick Massot (Oct 01 2018 at 08:50):

But I hope the topology proof won't become ugly

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

Patrick Massot (Oct 01 2018 at 08:52):

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

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.

Patrick Massot (Oct 01 2018 at 11:28):

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

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?

Patrick Massot (Oct 01 2018 at 11:31):

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

Johannes Hölzl (Oct 01 2018 at 11:32):

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

Patrick Massot (Oct 01 2018 at 11:33):

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

Patrick Massot (Oct 01 2018 at 11:33):

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

Patrick Massot (Oct 01 2018 at 11:34):

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

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.

Patrick Massot (Oct 01 2018 at 11:35):

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

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

Patrick Massot (Oct 01 2018 at 11:36):

that you've hidden in mem_closure

Patrick Massot (Oct 01 2018 at 11:37):

also that name is much harder to find than image_closure_subset_closure_image

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.

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.

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

Patrick Massot (Oct 01 2018 at 13:37):

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

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?

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

Patrick Massot (Oct 01 2018 at 19:02):

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

Patrick Massot (Oct 01 2018 at 19:03):

Do we have open maps in mathlib?

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.

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?

Chris Hughes (Oct 01 2018 at 19:24):

use show

Johannes Hölzl (Oct 01 2018 at 19:26):

dsimp could also help.

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?

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?

Patrick Massot (Oct 01 2018 at 19:35):

yes, every group is normal in this case

Johannes Hölzl (Oct 01 2018 at 19:38):

so you can use quotient_add_group?

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

Patrick Massot (Oct 01 2018 at 19:40):

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

Patrick Massot (Oct 01 2018 at 19:41):

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

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

Patrick Massot (Oct 01 2018 at 19:46):

Patrick Massot (Oct 01 2018 at 19:52):

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

Johannes Hölzl (Oct 01 2018 at 19:57):

maybe its somewhere else?

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}

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

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.

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}

Johan Commelin (Oct 03 2018 at 16:23):

@Patrick Massot Do you have a strategy in mind?

Johan Commelin (Oct 03 2018 at 16:23):

Which ingredients would you want to apply?

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

Johan Commelin (Oct 03 2018 at 16:25):

Of course this is very vague...

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

Reid Barton (Oct 03 2018 at 17:22):

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

Reid Barton (Oct 03 2018 at 17:24):

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

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.

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.

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?

Reid Barton (Oct 03 2018 at 17:43):

Assuming "ctu" = continuous then continuous_quot_mk

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)

Reid Barton (Oct 03 2018 at 17:46):

For continuous_neg, you can argue along those lines.

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

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?

Patrick Massot (Oct 03 2018 at 18:48):

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

Patrick Massot (Oct 03 2018 at 18:50):

I'm waiting for mathlib to compile...

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

Patrick Massot (Oct 03 2018 at 18:55):

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

Reid Barton (Oct 03 2018 at 19:21):

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

Reid Barton (Oct 03 2018 at 19:23):

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

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

Patrick Massot (Oct 03 2018 at 19:26):

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

Patrick Massot (Oct 03 2018 at 19:27):

I need to think on paper

Patrick Massot (Oct 03 2018 at 19:53):

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

Kenny Lau (Oct 03 2018 at 19:55):

why do I feel like I've proved that

Patrick Massot (Oct 03 2018 at 19:55):

I'd be very interested

Patrick Massot (Oct 03 2018 at 19:55):

Do you remember if this is in mathlib?

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

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

Kenny Lau (Oct 03 2018 at 20:00):

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

Kenny Lau (Oct 03 2018 at 20:01):

@Patrick Massot is this what you want?

Patrick Massot (Oct 03 2018 at 20:01):

it looks very much like what I want

Kenny Lau (Oct 03 2018 at 20:02):

nice

Patrick Massot (Oct 03 2018 at 20:02):

I mean the statement of course

Kenny Lau (Oct 03 2018 at 20:02):

I mean, it's not hard to prove

Patrick Massot (Oct 03 2018 at 20:02):

the proof...

Kenny Lau (Oct 03 2018 at 20:03):

a first year could learn that

Patrick Massot (Oct 03 2018 at 20:03):

the math proof is easy yes

Patrick Massot (Oct 03 2018 at 20:04):

reading a term mode proof is hard (for me)

Kenny Lau (Oct 03 2018 at 20:04):

this proof is 3 months old btw

Patrick Massot (Oct 03 2018 at 20:06):

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

Patrick Massot (Oct 03 2018 at 20:06):

but it's still helpful to have one full proof

Kenny Lau (Oct 03 2018 at 20:07):

Patrick Massot (Oct 03 2018 at 20:08):

thanks!

Patrick Massot (Oct 03 2018 at 20:11):

Did you think about PRing stuff from this repo?

Kenny Lau (Oct 03 2018 at 20:11):

maybe

Patrick Massot (Oct 03 2018 at 20:20):

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

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.

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

Kevin Buzzard (Oct 04 2018 at 06:41):

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

Last updated: Dec 20 2023 at 11:08 UTC