## Stream: maths

### Topic: quotient_group.inc

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


looks good to me

#### Patrick Massot (Feb 26 2019 at 08:52):

why is it called inc?

#### Johan Commelin (Feb 26 2019 at 08:54):

why is it called inc?

for "inclusion"

#### Mario Carneiro (Feb 26 2019 at 08:55):

this doesn't look like an inclusion to me

#### Mario Carneiro (Feb 26 2019 at 08:55):

to me inclusion = subtype.val

#### Mario Carneiro (Feb 26 2019 at 08:55):

and this is a quotient not a subtype

#### Mario Carneiro (Feb 26 2019 at 08:56):

I would just call it lift_ker or something

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

#### Mario Carneiro (Feb 26 2019 at 08:56):

actually ker_lift is better

#### Mario Carneiro (Feb 26 2019 at 08:56):

lift_ker would be a theorem about the kernel of lift

#### Johan Commelin (Feb 26 2019 at 08:57):

Ok, I will prepare a PR

#### Kevin Buzzard (Feb 26 2019 at 09:00):

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

#### Kevin Buzzard (Feb 26 2019 at 09:01):

line 82 of group_theory/quotient_group.lean maybe

#### Kevin Buzzard (Feb 26 2019 at 09:02):

injectivity is line 127

#### Johan Commelin (Feb 26 2019 at 09:08):

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

#### Kevin Buzzard (Feb 26 2019 at 09:14):

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

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

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

#### Kevin Buzzard (Feb 26 2019 at 09:20):

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

#### 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]

#### Kevin Buzzard (Feb 26 2019 at 09:22):

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

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

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

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

#### Kevin Buzzard (Feb 26 2019 at 09:29):

It's called descent in mathematics

#### Mario Carneiro (Feb 26 2019 at 09:29):

lift means construct a function via the universal property

#### Kevin Buzzard (Feb 26 2019 at 09:29):

It's an entire subject area

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

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

#### Mario Carneiro (Feb 26 2019 at 09:30):

humans are inconsistent like that

#### Kevin Buzzard (Feb 26 2019 at 09:31):

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

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

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

#### Mario Carneiro (Feb 26 2019 at 09:32):

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

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

#### Mario Carneiro (Feb 26 2019 at 09:33):

That sounds like map to me

#### Kevin Buzzard (Feb 26 2019 at 09:33):

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

#### Johan Commelin (Feb 26 2019 at 09:34):

We draw this like so:

Y
|
v
X


and hence stuff descends from Y to X.

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

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

#### Mario Carneiro (Feb 26 2019 at 09:35):

map and lift aren't the same in this world

#### Kevin Buzzard (Feb 26 2019 at 09:35):

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

#### Kevin Buzzard (Feb 26 2019 at 09:35):

and all the terminology is led by that picture

#### Mario Carneiro (Feb 26 2019 at 09:35):

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

#### Kevin Buzzard (Feb 26 2019 at 09:35):

Mario I think you have the wrong X and Y

Y = X / ~

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


#### Kevin Buzzard (Feb 26 2019 at 09:36):

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

#### Kevin Buzzard (Feb 26 2019 at 09:36):

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

#### Mario Carneiro (Feb 26 2019 at 09:36):

In my example F is quotient

#### Mario Carneiro (Feb 26 2019 at 09:37):

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

#### Mario Carneiro (Feb 26 2019 at 09:37):

that's just the general shape of the definition

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

#### Mario Carneiro (Feb 26 2019 at 09:37):

It's standard lean terminology

#### Kevin Buzzard (Feb 26 2019 at 09:38):

I know, and this is unfortunate.

#### Kevin Buzzard (Feb 26 2019 at 09:38):

That's what I'm saying.

#### Patrick Massot (Feb 26 2019 at 09:38):

In this sentence, Lean means Mario, right?

#### Kevin Buzzard (Feb 26 2019 at 09:38):

quotient.lift is in core

#### Mario Carneiro (Feb 26 2019 at 09:38):

No, quot.lift predates me significantly

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

#### Mario Carneiro (Feb 26 2019 at 09:39):

I think the math terminology for this is inconsistent

#### Mario Carneiro (Feb 26 2019 at 09:39):

based on what you've all said

#### Kevin Buzzard (Feb 26 2019 at 09:39):

How can "always call it descent" be inconsistent?

#### Mario Carneiro (Feb 26 2019 at 09:40):

because it's not always called descent

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

#### Kevin Buzzard (Feb 26 2019 at 09:40):

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

#### Kevin Buzzard (Feb 26 2019 at 09:40):

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

I get that

#### Kevin Buzzard (Feb 26 2019 at 09:40):

and we were first and there are far more of us

#### Kevin Buzzard (Feb 26 2019 at 09:40):

so it's unfortunate

#### Mario Carneiro (Feb 26 2019 at 09:40):

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

and co stuff

#### Kevin Buzzard (Feb 26 2019 at 09:41):

I am not clear what you mean

#### Kevin Buzzard (Feb 26 2019 at 09:41):

Is there limit.lift?

#### Kevin Buzzard (Feb 26 2019 at 09:41):

I am specifically talking about quotients.

#### Mario Carneiro (Feb 26 2019 at 09:41):

I'm not, that's my point

#### Kevin Buzzard (Feb 26 2019 at 09:42):

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

#### Mario Carneiro (Feb 26 2019 at 09:42):

I want a standard terminology across domains

#### Kevin Buzzard (Feb 26 2019 at 09:42):

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

#### Mario Carneiro (Feb 26 2019 at 09:42):

the map into a limit?

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

#### Kevin Buzzard (Feb 26 2019 at 09:43):

Is this called lift in Lean?

#### Kevin Buzzard (Feb 26 2019 at 09:43):

That's called "universal property" in maths

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

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

#### Kevin Buzzard (Feb 26 2019 at 09:44):

which I am arguing should be callde quotient.descent

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

#### Kevin Buzzard (Feb 26 2019 at 09:45):

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

#### Johan Commelin (Feb 26 2019 at 09:45):

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

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

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

#### Johan Commelin (Feb 26 2019 at 09:47):

So we should rename those (-;

#### Mario Carneiro (Feb 26 2019 at 09:47):

limit does actually have a field called lift

#### Johan Commelin (Feb 26 2019 at 09:47):

And colimit has a field called desc

#### Mario Carneiro (Feb 26 2019 at 09:47):

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

#### Kevin Buzzard (Feb 26 2019 at 09:47):

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

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

#### Mario Carneiro (Feb 26 2019 at 09:48):

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

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

#### Kevin Buzzard (Feb 26 2019 at 09:48):

Universe lifting always sounded sensible to me.

#### Kevin Buzzard (Feb 26 2019 at 09:48):

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

Sure

#### Mario Carneiro (Feb 26 2019 at 09:49):

I agree, I'm not advocating any changes there

#### Mario Carneiro (Feb 26 2019 at 09:49):

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

#### Kevin Buzzard (Feb 26 2019 at 09:49):

so you're advocating inconsistent usage of lift?

#### Kevin Buzzard (Feb 26 2019 at 09:49):

as opposed to a sensible renaming of quotient.lift?

#### Mario Carneiro (Feb 26 2019 at 09:49):

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

#### Patrick Massot (Feb 26 2019 at 09:50):

mathlib can still define an alias, right?

#### Patrick Massot (Feb 26 2019 at 09:50):

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

#### Mario Carneiro (Feb 26 2019 at 09:50):

Actually you'd best fix it before lean 4

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

#### Mario Carneiro (Feb 26 2019 at 09:51):

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

#### Kevin Buzzard (Feb 26 2019 at 09:51):

Not if Leo takes our side

#### Kevin Buzzard (Feb 26 2019 at 09:51):

I had always assumed that lift was a CS standard

#### Mario Carneiro (Feb 26 2019 at 09:51):

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

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

#### Mario Carneiro (Feb 26 2019 at 09:52):

I just came here and learned the language

#### Mario Carneiro (Feb 26 2019 at 09:52):

but I do think that we should strive for consistency regardless

#### Patrick Massot (Feb 26 2019 at 09:53):

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

#### Mario Carneiro (Feb 26 2019 at 09:53):

again, across domains consistency

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

in both diagrams

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

To define the map from L to N you have to descend elements from F(X) downwards to L.

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

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

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

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

#### Johan Commelin (Feb 26 2019 at 10:06):

And not only in our heads, also in Lean.

#### Johan Commelin (Feb 26 2019 at 10:06):

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

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

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

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

#### Mario Carneiro (Feb 26 2019 at 10:08):

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

#### Patrick Massot (Feb 26 2019 at 10:08):

I never saw ⊂ meaning strict inclusion before using Lean

#### 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 ⊂

#### Mario Carneiro (Feb 26 2019 at 10:10):

I grant that this is a dumb choice of abbreviation

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

#### Patrick Massot (Feb 26 2019 at 10:12):

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

#### Patrick Massot (Feb 26 2019 at 10:12):

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

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

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

#### Johan Commelin (Feb 26 2019 at 10:13):

Hehe, we're also nonstrict :see_no_evil:

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

#### Patrick Massot (Feb 26 2019 at 10:16):

Do you actually write ⊆ on blackboards?

I certainly do

#### Mario Carneiro (Feb 26 2019 at 10:17):

Do you write a line under the <= symbol?

#### Patrick Massot (Feb 26 2019 at 10:22):

Why would I do that?

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

#### Johan Commelin (Feb 26 2019 at 10:23):

You want your students to write 1 ≤ 1.

#### Patrick Massot (Feb 26 2019 at 10:24):

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

#### Patrick Massot (Feb 26 2019 at 10:26):

In France we use ⩽ instead of the ugly ≤

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

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

#### Mario Carneiro (Feb 26 2019 at 10:38):

wait, that sounds the opposite of johan's description

#### Mario Carneiro (Feb 26 2019 at 10:39):

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

no it's not

gah!

#### Sebastien Gouezel (Feb 26 2019 at 10:39):

It depends on F.

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

double gah

#### Patrick Massot (Feb 26 2019 at 10:40):

Let me find my ascii art again

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

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


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

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

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

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

#### Kevin Buzzard (Feb 26 2019 at 11:43):

[sorry, I was just catching up]

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

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

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

#### Kevin Buzzard (Feb 26 2019 at 11:47):

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

#### Kevin Buzzard (Feb 26 2019 at 11:47):

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

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

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

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

#### Mario Carneiro (Feb 26 2019 at 11:58):

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

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

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

#### Mario Carneiro (Feb 26 2019 at 12:02):

you might have Y being the free object over X

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

#### Kevin Buzzard (Feb 26 2019 at 12:03):

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

#### Kevin Buzzard (Feb 26 2019 at 12:04):

The term is used vaguely in mathematics I suspect.

#### Kevin Buzzard (Feb 26 2019 at 12:04):

Descent theory is an actual thing though

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

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

#### Johan Commelin (Feb 26 2019 at 12:06):

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

#### Johan Commelin (Feb 26 2019 at 12:06):

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

#### Mario Carneiro (Feb 26 2019 at 12:06):

it will be called descent of course

#### Mario Carneiro (Feb 26 2019 at 12:07):

actually I'm not sure there is anything to name

#### Mario Carneiro (Feb 26 2019 at 12:07):

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

#### Mario Carneiro (Feb 26 2019 at 12:07):

most of the names have to do with particular operations

#### Mario Carneiro (Feb 26 2019 at 12:08):

The descent page doesn't really have anything formalizable

#### Mario Carneiro (Feb 26 2019 at 12:08):

it seems more like a setting, in the literary sense

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

#### 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!

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

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