Zulip Chat Archive

Stream: maths

Topic: quotient_group.inc


view this post on Zulip Johan Commelin (Feb 26 2019 at 08:49):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 08:52):

looks good to me

view this post on Zulip Patrick Massot (Feb 26 2019 at 08:52):

why is it called inc?

view this post on Zulip Johan Commelin (Feb 26 2019 at 08:54):

why is it called inc?

for "inclusion"

view this post on Zulip Mario Carneiro (Feb 26 2019 at 08:55):

this doesn't look like an inclusion to me

view this post on Zulip Mario Carneiro (Feb 26 2019 at 08:55):

to me inclusion = subtype.val

view this post on Zulip Mario Carneiro (Feb 26 2019 at 08:55):

and this is a quotient not a subtype

view this post on Zulip Mario Carneiro (Feb 26 2019 at 08:56):

I would just call it lift_ker or something

view this post on Zulip Johan Commelin (Feb 26 2019 at 08:56):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 08:56):

actually ker_lift is better

view this post on Zulip Mario Carneiro (Feb 26 2019 at 08:56):

lift_ker would be a theorem about the kernel of lift

view this post on Zulip Johan Commelin (Feb 26 2019 at 08:57):

Ok, I will prepare a PR

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:00):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:01):

line 82 of group_theory/quotient_group.lean maybe

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:02):

injectivity is line 127

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:03):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 09:08):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:14):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:16):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:18):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:20):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:20):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:22):

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

view this post on Zulip Patrick Massot (Feb 26 2019 at 09:25):

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"?

view this post on Zulip Patrick Massot (Feb 26 2019 at 09:26):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:29):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:29):

It's called descent in mathematics

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:29):

lift means construct a function via the universal property

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:29):

It's an entire subject area

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:30):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:30):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:30):

humans are inconsistent like that

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:31):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 09:31):

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/*

view this post on Zulip Patrick Massot (Feb 26 2019 at 09:32):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:32):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:33):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:33):

That sounds like map to me

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:33):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 09:34):

We draw this like so:

Y
|
v
X

and hence stuff descends from Y to X.

view this post on Zulip Patrick Massot (Feb 26 2019 at 09:34):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:34):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:35):

map and lift aren't the same in this world

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:35):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:35):

and all the terminology is led by that picture

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:35):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:35):

Mario I think you have the wrong X and Y

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:36):

Y = X / ~

view this post on Zulip Patrick Massot (Feb 26 2019 at 09:36):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:36):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:36):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:36):

In my example F is quotient

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:37):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:37):

that's just the general shape of the definition

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:37):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:37):

It's standard lean terminology

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:38):

I know, and this is unfortunate.

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:38):

That's what I'm saying.

view this post on Zulip Patrick Massot (Feb 26 2019 at 09:38):

In this sentence, Lean means Mario, right?

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:38):

quotient.lift is in core

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:38):

No, quot.lift predates me significantly

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:39):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:39):

I think the math terminology for this is inconsistent

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:39):

based on what you've all said

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:39):

How can "always call it descent" be inconsistent?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:40):

because it's not always called descent

view this post on Zulip Patrick Massot (Feb 26 2019 at 09:40):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:40):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:40):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:40):

I get that

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:40):

and we were first and there are far more of us

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:40):

so it's unfortunate

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:40):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:41):

and co stuff

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:41):

I am not clear what you mean

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:41):

Is there limit.lift?

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:41):

I am specifically talking about quotients.

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:41):

I'm not, that's my point

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:42):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:42):

I want a standard terminology across domains

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:42):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:42):

the map into a limit?

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:43):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:43):

Is this called lift in Lean?

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:43):

That's called "universal property" in maths

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:44):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:44):

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"

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:44):

which I am arguing should be callde quotient.descent

view this post on Zulip Johan Commelin (Feb 26 2019 at 09:45):

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.

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:45):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 09:45):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:45):

That norm extends to padic_norm_e

view this post on Zulip Johan Commelin (Feb 26 2019 at 09:47):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:47):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 09:47):

So we should rename those (-;

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:47):

limit does actually have a field called lift

view this post on Zulip Johan Commelin (Feb 26 2019 at 09:47):

And colimit has a field called desc

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:47):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:47):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:48):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:48):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 09:48):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:48):

Universe lifting always sounded sensible to me.

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:48):

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

view this post on Zulip Patrick Massot (Feb 26 2019 at 09:48):

Sure

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:49):

I agree, I'm not advocating any changes there

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:49):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:49):

so you're advocating inconsistent usage of lift?

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:49):

as opposed to a sensible renaming of quotient.lift?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:49):

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

view this post on Zulip Patrick Massot (Feb 26 2019 at 09:50):

mathlib can still define an alias, right?

view this post on Zulip Patrick Massot (Feb 26 2019 at 09:50):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:50):

Actually you'd best fix it before lean 4

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:51):

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?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:51):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:51):

Not if Leo takes our side

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:51):

I had always assumed that lift was a CS standard

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:51):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:51):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:52):

I just came here and learned the language

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:52):

but I do think that we should strive for consistency regardless

view this post on Zulip Patrick Massot (Feb 26 2019 at 09:53):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:53):

again, across domains consistency

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:55):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 09:55):

in both diagrams

view this post on Zulip Johan Commelin (Feb 26 2019 at 09:59):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 10:00):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:01):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 10:04):

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?

view this post on Zulip Johan Commelin (Feb 26 2019 at 10:05):

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.

view this post on Zulip Johan Commelin (Feb 26 2019 at 10:06):

And not only in our heads, also in Lean.

view this post on Zulip Johan Commelin (Feb 26 2019 at 10:06):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:06):

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

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:06):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:07):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:08):

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

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:08):

I never saw meaning strict inclusion before using Lean

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:09):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:10):

I grant that this is a dumb choice of abbreviation

view this post on Zulip Johan Commelin (Feb 26 2019 at 10:11):

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.

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:12):

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

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:12):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:12):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:13):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 10:13):

Hehe, we're also nonstrict :see_no_evil:

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:15):

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

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:16):

Do you actually write ⊆ on blackboards?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:16):

I certainly do

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:17):

Do you write a line under the <= symbol?

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:22):

Why would I do that?

view this post on Zulip Johan Commelin (Feb 26 2019 at 10:23):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 10:23):

You want your students to write 1 ≤ 1.

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:24):

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

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:26):

In France we use instead of the ugly

view this post on Zulip Sebastien Gouezel (Feb 26 2019 at 10:35):

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.

view this post on Zulip Sebastien Gouezel (Feb 26 2019 at 10:37):

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.

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:38):

wait, that sounds the opposite of johan's description

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:39):

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

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:39):

no it's not

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:39):

gah!

view this post on Zulip Sebastien Gouezel (Feb 26 2019 at 10:39):

It depends on F.

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:40):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:40):

double gah

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:40):

Let me find my ascii art again

view this post on Zulip Sebastien Gouezel (Feb 26 2019 at 10:40):

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.

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:42):

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

\tilde M
  |
  V
  M -> R

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 11:38):

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.

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 11:39):

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.

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 11:41):

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?

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 11:43):

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.

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 11:43):

[sorry, I was just catching up]

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:45):

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?

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 11:46):

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.

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 11:46):

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.

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 11:47):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 11:47):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 11:48):

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.

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 11:50):

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.

view this post on Zulip Johan Commelin (Feb 26 2019 at 11:57):

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.

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:58):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 11:59):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:00):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:02):

you might have Y being the free object over X

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 12:03):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 12:03):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 12:04):

The term is used vaguely in mathematics I suspect.

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 12:04):

Descent theory is an actual thing though

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 12:05):

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

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:05):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:06):

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

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:06):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:06):

it will be called descent of course

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:07):

actually I'm not sure there is anything to name

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:07):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:07):

most of the names have to do with particular operations

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:08):

The descent page doesn't really have anything formalizable

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:08):

it seems more like a setting, in the literary sense

view this post on Zulip Jeremy Avigad (Feb 26 2019 at 14:57):

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.

view this post on Zulip Jeremy Avigad (Feb 26 2019 at 15:05):

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!

view this post on Zulip Reid Barton (Feb 26 2019 at 16:04):

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.

view this post on Zulip Reid Barton (Feb 26 2019 at 16:05):

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


Last updated: May 09 2021 at 10:11 UTC