quotient_group.inc

Stream: maths

[Johan Commelin]

Is stuff like this considered useful for mathlib? In other words, should I PR this? @Chris Hughes @Mario Carneiro

import group_theory.quotient_group

universes u₁ u₂ u₃

open is_group_hom quotient_group function

variables {G₁ : Type u₁} [group G₁]
variables {G₂ : Type u₂} [group G₂]
variables (φ : G₁ → G₂) [is_group_hom φ]

def inc : quotient (ker φ) → G₂ :=
lift _ φ $ λ g, (mem_ker φ).mp

lemma inc_mk (g : G₁) : (inc φ) g = φ g :=
lift_mk _ _ _

lemma inc_mk' (g : G₁) : (inc φ) (mk g) = φ g :=
lift_mk' _ _ _

instance : is_group_hom (inc φ) :=
quotient_group.is_group_hom_quotient_lift _ _ _

lemma inc_injective : injective (inc φ) :=
assume a b, quotient.induction_on₂' a b $
assume a b (h : φ a = φ b), quotient.sound' $
show a⁻¹ * b ∈ ker φ,
by rw [mem_ker φ, is_group_hom.mul φ, ← h, is_group_hom.inv φ, inv_mul_self]

section
variables {N₁ : set G₁} [normal_subgroup N₁]
variables {N₂ : set G₂} [normal_subgroup N₂]

instance map_is_group_hom (h : N₁ ⊆ φ ⁻¹' N₂) : is_group_hom (map _ _ φ h) :=
quotient_group.is_group_hom_quotient_lift _ _ _

end

[Mario Carneiro]

looks good to me

[Patrick Massot]

why is it called inc?

[Johan Commelin]

why is it called inc?

for "inclusion"

[Mario Carneiro]

this doesn't look like an inclusion to me

[Mario Carneiro]

to me inclusion = subtype.val

[Mario Carneiro]

and this is a quotient not a subtype

[Mario Carneiro]

I would just call it lift_ker or something

[Johan Commelin]

Ok, so how should this called?
(It's a canonical injective map... I'm used to calling those inclusion...)

[Mario Carneiro]

actually ker_lift is better

[Mario Carneiro]

lift_ker would be a theorem about the kernel of lift

[Johan Commelin]

Ok, I will prepare a PR

[Kevin Buzzard]

I have this vague memory that this stuff is already there...

[Kevin Buzzard]

line 82 of group_theory/quotient_group.lean maybe

[Kevin Buzzard]

injectivity is line 127

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/blob/71a7e1c497336b2eeae75cc8a54bb4ada32ca0f7/src/group_theory/quotient_group.lean#L127 and surrounding stuff

[Johan Commelin]

Aah, good catch. So maybe it doesn't even deserve its own name...

[Kevin Buzzard]

I wouldn't trust the naming conventions of the people who wrote that file ;-)

[Kevin Buzzard]

In fact IIRC I just took quotient_module.lean and ported it to groups, initially, and quotient_module.lean was written by Johannes...wait...where did _quotient_module.lean go? I was going to say "you should look there".

[Kevin Buzzard]

From https://github.com/leanprover-community/mathlib/blob/master/docs/theories/relations.md : "A nice mathematical example can be found in linear_algebra/quotient_module". Hmm...

[Kevin Buzzard]

How do I do "go back to Sept 2018" in git/github?

[Kevin Buzzard]

[to find the definition I was talking about so I can search for it to find out where it went]

[Kevin Buzzard]

Oh cool, I can switch to the commit when relations.md was added

[Patrick Massot]

I wouldn't trust the naming conventions of the people who wrote that file ;-)

Are we talking about people who use "lifs" to mean "descends"?

[Patrick Massot]

I don't remember if we already asked: if this lift crazyness a standard for all proof assistants, or is it only in Lean?

[Mario Carneiro]

I don't know any other system that uses this particular terminology, but it also makes sense to me

[Kevin Buzzard]

It's called descent in mathematics

[Mario Carneiro]

lift means construct a function via the universal property

[Kevin Buzzard]

It's an entire subject area

[Kevin Buzzard]

descent means construct a function on a quotient from a function on the top which is symmetric

[Mario Carneiro]

I think this is actually called lift in many contexts, although I wouldn't be surprised if for quotients the terminology is different

[Mario Carneiro]

humans are inconsistent like that

[Kevin Buzzard]

https://mathoverflow.net/questions/22032/what-is-descent-theory

[Johan Commelin]

I guess mathematicians expect lift for the universal property of a limit, and desc for the universal property of a colimit. Exactly the way we have it currently in category_theory/*

[Patrick Massot]

Kevin, your link is too specialized, we are talking about the very elementary notion of function induced on quotients

[Mario Carneiro]

If that's how this works I would have preferred colift

[Kevin Buzzard]

My link is super-general -- we have a morphism Y -> X in a category and we want some "object defined on Y" (e.g. a function or predicate) to descend to an "object defined on X".

[Mario Carneiro]

That sounds like map to me

[Kevin Buzzard]

that's lift in this world, isn't it?

[Johan Commelin]

We draw this like so:

Y
|
v
X

and hence stuff descends from Y to X.

[Patrick Massot]

What makes this mathlib terminology really confusing is that we also use lift in math, especially to denote the opposite operation. If a function is defined on a quotient, we can try to lift it to the object before quotienting

[Kevin Buzzard]

Descent theory gives you conditions on the structure defined on Y to descend to an structure defined on X

[Mario Carneiro]

map and lift aren't the same in this world

[Kevin Buzzard]

Johan is right -- mathematicians draw the quotient map as a downwards arrow typically.

[Kevin Buzzard]

and all the terminology is led by that picture

[Mario Carneiro]

roughly speaking map : (X -> Y) -> F X -> F Y and lift : (X -> Y) -> F X -> Y

[Kevin Buzzard]

Mario I think you have the wrong X and Y

[Kevin Buzzard]

Y = X / ~

[Patrick Massot]

Johan is right, this terminology is tied to the way we draw diagrams. For instance, if we have a covering map Y -> X, and a map from Z to X, lifting this map to Y means finding an arrow from lower left to upper right in:

     Y
     |
     V
Z -> X

[Kevin Buzzard]

lift : (X -> Z) -> (Y -> Z)

[Kevin Buzzard]

so we descend the map X -> Z to a map Y -> Z

[Mario Carneiro]

In my example F is quotient

[Mario Carneiro]

I'm not saying it's a functor or anything

[Mario Carneiro]

that's just the general shape of the definition

[Kevin Buzzard]

If "lift" is not some standard CS terminology then it's hard for us to see why you're using it when it is in direct contradiction with the standard maths terminology

[Mario Carneiro]

It's standard lean terminology

[Kevin Buzzard]

I know, and this is unfortunate.

[Kevin Buzzard]

That's what I'm saying.

[Patrick Massot]

In this sentence, Lean means Mario, right?

[Kevin Buzzard]

quotient.lift is in core

[Mario Carneiro]

No, quot.lift predates me significantly

[Mario Carneiro]

I have no idea what the standard math terminology is but I like to have a standard and stick to it, and this works as good as any

[Mario Carneiro]

I think the math terminology for this is inconsistent

[Mario Carneiro]

based on what you've all said

[Kevin Buzzard]

How can "always call it descent" be inconsistent?

[Mario Carneiro]

because it's not always called descent

[Patrick Massot]

I don't see how this "works as good as any": it confuses every mathematician and is not especially illuminating to computer scientists

[Kevin Buzzard]

It's not map, you've misunderstood what I'm saying

[Kevin Buzzard]

what we call descent is what you call quot.lift.

[Mario Carneiro]

I get that

[Kevin Buzzard]

and we were first and there are far more of us

[Kevin Buzzard]

so it's unfortunate

[Mario Carneiro]

but you can lift more things than just quotients. What about limits and pullbacks and products?

[Mario Carneiro]

and co stuff

[Kevin Buzzard]

I am not clear what you mean

[Kevin Buzzard]

Is there limit.lift?

[Kevin Buzzard]

I am specifically talking about quotients.

[Mario Carneiro]

I'm not, that's my point

[Kevin Buzzard]

What is an example of usage of lift outside the quotient setting?

[Mario Carneiro]

I want a standard terminology across domains

[Kevin Buzzard]

So what is an example of usage of lift outside the quotient setting?

[Mario Carneiro]

the map into a limit?

[Kevin Buzzard]

We have maps from A to X_i and we deduce a map from A to X, the limit of the X_i?

[Kevin Buzzard]

Is this called lift in Lean?

[Kevin Buzzard]

That's called "universal property" in maths

[Kevin Buzzard]

I don't recall lift being used for this notion in Lean. My issue is specifically with the naming of quotient.lift.

[Mario Carneiro]

From padic stuff:

• Fix p and [prime p]. padic_rationals.lean defines ℚ_[p] as the Cauchy completion of
  ℚ wrt padic_norm p using the same mechanisms as data/real/basic.lean. It is immediately a
  field. The norm lifts to padic_norm_e : ℚ_[p] → ℚ, which is cast to ℝ and gives us a
  normed_field instance. ℚ_[p] is shown to be Cauchy complete.

Lifts here is used to mean "extend to this free construction"

[Kevin Buzzard]

which I am arguing should be callde quotient.descent

[Johan Commelin]

Mario, I would really argue for have a distinction between the limit/colimit terminology. So maps into a limit are called lift, we wont complain.
The whole difference is whether you are mapping into or out of something.

[Kevin Buzzard]

I suspect that p-adic stuff was written by a computer scientist :-)

[Johan Commelin]

lift means you map into something.
desc or colift means you map out of something.

[Kevin Buzzard]

That norm extends to padic_norm_e

[Johan Commelin]

And even if you would say that the "norm descends to padic_norm_e" then it would be less confusing to mathematicians

[Mario Carneiro]

lift is used in a few places to mean something more like map, i.e. ulift and plift, preorder.lift, etc

[Johan Commelin]

So we should rename those (-;

[Mario Carneiro]

limit does actually have a field called lift

[Johan Commelin]

And colimit has a field called desc

[Mario Carneiro]

(I'm just looking at current uses in lean right now)

[Kevin Buzzard]

Are you just looking through the entire source code for lifts to justify your position? :-)

[Kevin Buzzard]

Then if that's all you can come up with, I think your argument is very weak.

[Mario Carneiro]

I want to find out if it is actually being used in a consistent way

[Johan Commelin]

@Mario Carneiro We are very happy with limit.lift. The point is that quotient.lift goes in the opposite direction.

[Kevin Buzzard]

Universe lifting always sounded sensible to me.

[Kevin Buzzard]

I always imagine the bigger universe as sitting over the smaller one

[Patrick Massot]

Sure

[Mario Carneiro]

I agree, I'm not advocating any changes there

[Mario Carneiro]

but it's an interesting thing to note how terminology can clash

[Kevin Buzzard]

so you're advocating inconsistent usage of lift?

[Kevin Buzzard]

as opposed to a sensible renaming of quotient.lift?

[Mario Carneiro]

quot.lift isn't just in core; it's literally baked into lean

[Patrick Massot]

mathlib can still define an alias, right?

[Patrick Massot]

And when the great time of Lean 4 comes, we'll ask very politely.

[Mario Carneiro]

Actually you'd best fix it before lean 4

[Kevin Buzzard]

Unfortunately the real world is calling me. But at this point I did not yet see a coherent argument for the quot.lift name. Mario -- would Jeremy have an opinion on this issue?

[Mario Carneiro]

you can fix it now, when lean 4 comes around it will get un-fixed

[Kevin Buzzard]

Not if Leo takes our side

[Kevin Buzzard]

I had always assumed that lift was a CS standard

[Mario Carneiro]

I don't know what Jeremy's position is on this

[Kevin Buzzard]

but now I discover that it's not I think there's a case for arguing for a change.

[Mario Carneiro]

I just came here and learned the language

[Mario Carneiro]

but I do think that we should strive for consistency regardless

[Patrick Massot]

Yes, let's consistently use "descends" instead of "lifts"

[Mario Carneiro]

again, across domains consistency

[Mario Carneiro]

I keep staring at the pictures in https://en.wikipedia.org/wiki/Limit_(category_theory) to see the geometric intuition, but all the arrows go down

[Mario Carneiro]

in both diagrams

[Johan Commelin]

@Mario Carneiro Take the limit diagram: https://upload.wikimedia.org/wikipedia/commons/8/81/Functor_cone_%28extended%29.svg
To define the map from N to L you have to lift elements from F(X) upwards to L.

Take the colimit diagram: https://upload.wikimedia.org/wikipedia/commons/5/5a/Functor_co-cone_%28extended%29.svg
To define the map from L to N you have to descend elements from F(X) downwards to L.

[Johan Commelin]

Like I said, it is really a matter of whether you are mapping into, or out of something.

[Mario Carneiro]

But you are making a function from L, so elements of L have to lift(?) to elements of F(X) to be mapped

[Johan Commelin]

Do you agree that it is useful to call cokernels what they are? Or would you rather call them kernels? Similar for (co)product, and generally for (co)limit?

[Johan Commelin]

Anyway, most of this is just history... for ages we have called limity things lift and colimity things desc, so it is confusing for us to see the two names being merged. They are dual things in our heads.

[Johan Commelin]

And not only in our heads, also in Lean.

[Johan Commelin]

Its just that the Lean-terminology doesn't reflect this duality.

[Mario Carneiro]

I think having a different name for product and coproduct is important because they both exist and are different

[Patrick Massot]

I'm reading all that while typing explanation for my students about how Lean means ⊊ when it writes ⊂, and means ⊂ when it writes ⊆. Sometimes life is difficult...

[Mario Carneiro]

but I would be okay with product.universal_thing and coproduct.universal_thing rather than coproduct.couniversal_cothing

[Mario Carneiro]

eww, you're one of those people? Nonstrict ⊂ should die

[Patrick Massot]

I never saw ⊂ meaning strict inclusion before using Lean

[Patrick Massot]

And it took me a while to realize what was Lean's problem, especially when VScode happily uses \subset to trigger ⊂

[Mario Carneiro]

I grant that this is a dumb choice of abbreviation

[Johan Commelin]

Hmm if limit.lift were called limit.ump (for universal mapping property) and colimit.desc were called colimit.ump, I don't think I would complain, and I would also not find it confusing.
Similarly quot.ump or quotient.ump doesn't cause me any cognitive dissonance. It's way way better than quot.lift.

[Patrick Massot]

Is this an international issue? Do you actually use ⊆ everywhere in the US?

[Patrick Massot]

Johan, how do you denote set inclusion in the Netherlands and in Germany?

[Mario Carneiro]

Most neutral sources will just use ⊊ and ⊆, but among choices for the meaning of ⊂ one is obviously better

[Mario Carneiro]

I think there is some historical tendency for ⊂ as nonstrict, but like I said I'm happy to let it pass

[Johan Commelin]

Hehe, we're also nonstrict :see_no_evil:

[Mario Carneiro]

I think ⊆ is more common than ⊂ around here to denote nonstrict subset, probably because people recognize the ambiguity and don't want to engage, which is fine

[Patrick Massot]

Do you actually write ⊆ on blackboards?

[Mario Carneiro]

I certainly do

[Mario Carneiro]

Do you write a line under the <= symbol?

[Patrick Massot]

Why would I do that?

[Johan Commelin]

@Patrick Massot I think Mario means that you wouldn't allow yourself to write 1 < 1, but you do allow X \subset X.

[Johan Commelin]

You want your students to write 1 ≤ 1.

[Patrick Massot]

Oh I see! I thought this <= was ascii art for an implication from right to left

[Patrick Massot]

In France we use ⩽ instead of the ugly ≤

[Sebastien Gouezel]

I'm arriving a little bit too late, but I just want to add that to me also quot.lift is crazy, and if there's a possibility ot change it I will support it very strongly.

[Sebastien Gouezel]

In geometry, if tilde M is the universal cover of M, then a function M -> R lifts to a function tildeM -> R (by composing by the canonical projection), and a function tilde M -> R which is constant on fibers descends to a function M -> R. This corresponds to the picture that tildeM sits above M.

[Mario Carneiro]

wait, that sounds the opposite of johan's description

[Mario Carneiro]

I thought (X -> Y) -> F X -> Y is supposed to be called descent

[Patrick Massot]

no it's not

[Mario Carneiro]

gah!

[Sebastien Gouezel]

It depends on F.

[Patrick Massot]

and it's the same example that I gave (when I fighted for 2 minutes before getting the ascii art right)

[Mario Carneiro]

double gah

[Patrick Massot]

Let me find my ascii art again

[Sebastien Gouezel]

If F X is bigger than X, then its sits above X and you are lifting things. If it is smaller (a quotient, say), it sits below X and you have descends.

[Patrick Massot]

Sorry, my example was not exactly the same, but it's consistent

\tilde M
  |
  V
  M -> R

[Kevin Buzzard]

I'm reading all that while typing explanation for my students about how Lean means ⊊ when it writes ⊂, and means ⊂ when it writes ⊆. Sometimes life is difficult...

This is country-dependent I think, like how in the UK nat has no zero. In my papers I never write nat or ⊂ as I have plenty of evidence that mathematicians use them in more than one way so I regard them as overloaded and hence dangerous. I use ⊊ and ⊆ only.

[Kevin Buzzard]

I keep staring at the pictures in https://en.wikipedia.org/wiki/Limit_(category_theory) to see the geometric intuition, but all the arrows go down

As a general rule, bigger things go on top. But when you write the diagram representing the universal property, you just put the non-universal object in the place where the diagram becomes easiest to draw.

[Kevin Buzzard]

I never saw ⊂ meaning strict inclusion before using Lean

But you saw < meaning strict inequality, right? In Jantzen's book on algebraic groups he uses ⊂ to mean strict inclusion, and in John Thompson's group theory lectures I attended as an undergraduate he also used this convention. Maybe it's a US thing?

[Kevin Buzzard]

In geometry, if tilde M is the universal cover of M...

You see -- this notion of the big object lying above the smaller object is ubiquitous throughout maths. This is exactly why it's jarring for mathematicians to "lift" a predicate on the top to a predicate on the bottom.

[Kevin Buzzard]

[sorry, I was just catching up]

[Mario Carneiro]

Okay, so if I have a big object Y over a small object X, do we say that a map X -> Z lifts to Y -> Z? What about lifting Z -> X to Z -> Y?

[Kevin Buzzard]

If I am teaching Galois theory and I have the field extension Q(sqrt(2)) : Q, I write the Q(sqrt(2)) on top and the map goes upwards. If I am doing scheme theory and I have Spec(Q(sqrt(2)) / Spec(Q) then I write Spec(Q(sqrt(2)) on the top and the map goes downwards. I would pronounce both ":" and "/" as "over", meaning that the object on the left is over the object on the right, even though they correspond to different kind of maps. The "over / cover / descent / lift" terminology is ubiquitous and is all designed to represent the fact that the bigger object is on top of the smaller one.

[Kevin Buzzard]

Okay, so if I have a big object Y over a small object X, do we say that a map X -> Z lifts to Y -> Z?

I think I would say that X -> Z induces a map Y -> Z here.

[Kevin Buzzard]

The mathematical notation is consistent with the general convention that bigger things go on top.

[Kevin Buzzard]

The concept of "lift" in maths is covering several distinct concepts in type theory here.

[Kevin Buzzard]

So we cannot use "lift" for all of them. But our point is that you guys have chosen to use lift for something we would never use "lift" for.

[Kevin Buzzard]

Check out "lifting property" here: https://en.wikipedia.org/wiki/Projective_module . We have a surjection N -> M so mathematicians instinctively write N above M because N is bigger. We then lift a map P -> M to P -> N.

[Johan Commelin]

Okay, so if I have a big object Y over a small object X, do we say that a map X -> Z lifts to Y -> Z? What about lifting Z -> X to Z -> Y?

The map Y → Z is just composition, so we don't call it a lift... it's too cheap.
But going from Z → X to Z → Y is exactly what lifting is. And you need to work to make it happen.

[Mario Carneiro]

No, assume that the map goes in whatever direction makes this lifty thing not composition

[Johan Commelin]

You have Y over X, so typically Y → X, and then X → Z will give you a map Y → Z by composition.

[Johan Commelin]

But if you get Z → X, then you could ask for a lift Z → Y. And this is typically a non-trivial condition/fact.

[Mario Carneiro]

you might have Y being the free object over X

[Kevin Buzzard]

If the big thing Y is on top of the small thing X but there's an injection X -> Y, then one could ask if a map X -> Z extends to a map Y -> Z

[Kevin Buzzard]

I guess one could argue that this is also lifting a map.

[Kevin Buzzard]

The term is used vaguely in mathematics I suspect.

[Kevin Buzzard]

Descent theory is an actual thing though

[Kevin Buzzard]

https://en.wikipedia.org/wiki/Descent_(mathematics)

Right at the top -- "we think of Y as 'above' X"

[Mario Carneiro]

Of course it says that, "descent" is in the name so they have to motivate the picture

[Johan Commelin]

Yes, and when we want to PR this stuff some decade in the future...

[Johan Commelin]

We will get a comment "please change this to lift-theory"

[Mario Carneiro]

it will be called descent of course

[Mario Carneiro]

actually I'm not sure there is anything to name

[Mario Carneiro]

we don't collect theories except perhaps in the naming of files

[Mario Carneiro]

most of the names have to do with particular operations

[Mario Carneiro]

The descent page doesn't really have anything formalizable

[Mario Carneiro]

it seems more like a setting, in the literary sense

[Jeremy Avigad]

A historical note: the use of the term "lift" in Lean comes from this paper: http://www.cs.nott.ac.uk/~psztxa/publ/defquotients.pdf. I asked Thorsten about it, and he said there was no deep reason for the choice. He wasn't aware of the mathematical terminology, and said they chose the term in conformance with functional programming. (For example, Google just found this for me: https://stackoverflow.com/questions/2395697/what-is-lifting-in-haskell/2395956.)
Anyhow, others have also complained about the word "lift" with quotients.

[Jeremy Avigad]

FWIW, I also parse ⊂ as strict subset, but I recognize that the symbol is ambiguous and so follow Kevin's policy of using only ⊊ and ⊆. (In a similar way, avoid talking about the range of a function, and use "image" to denote the image of the function on the domain, and "codomain" to denote the intended target.) I am shocked to hear that British nats don't include zero. Poor zero!

[Reid Barton]

Usually there's not much risk of confusion because "is a subset of" is whichever symbol appears 99% of the time and "is a proper subset of" is the one which appears 1% of the time.

[Reid Barton]

For me, $\subset$ and $\subseteq$ are just typographic variants of the same symbol