# Zulip Chat Archive

## Stream: maths

### Topic: What is this lemma called?

#### Chris Hughes (Apr 23 2019 at 18:43):

What is this called and where does it go?

def map {X Y Z : Type*} (fxy : X ↪ Y) (fxz : X ↪ Z) (hYZ : (Z ↪ Y) → false) : Y ↪ Z lemma trans_map {X Y Z : Type*} (fxy : X ↪ Y) (fxz : X ↪ Z) (hYZ : (Z ↪ Y) → false) : fxy.trans (map fxy fxz hYZ) = fxz

#### Johan Commelin (Apr 23 2019 at 18:54):

Your `def`

seems incomplete...

#### Chris Hughes (Apr 23 2019 at 18:55):

It's the injective map that has the property given by the lemma.

#### Chris Hughes (Apr 23 2019 at 18:56):

Or an injective map with that property.

#### Johan Commelin (Apr 23 2019 at 18:57):

Is `embedding.trans`

what I would have called `embedding.comp`

?

#### Chris Hughes (Apr 23 2019 at 18:58):

Yes

#### Johan Commelin (Apr 23 2019 at 18:58):

Also... where does your `map`

come up in practice? I don't really understand what's going on...

#### Chris Hughes (Apr 23 2019 at 18:58):

It came up doing algebraic closure.

#### Johan Commelin (Apr 23 2019 at 18:59):

Would you mind copy-pasting the entire definition of `map`

? And more context if you want?

#### Chris Hughes (Apr 23 2019 at 19:00):

I have a bunch of field structures on subsets of a random type, ordering by subset and the inclusion map is a field homomorphism.

#### Chris Hughes (Apr 23 2019 at 19:00):

Doing zorn on this gives the algebraic closure.

#### Chris Hughes (Apr 23 2019 at 19:01):

But to prove it's algebraically closed, you need to adjoin a root to the algebraic closure and transfer the structure of this back to some superset of the algebraic closure in the "big type".

#### Johan Commelin (Apr 23 2019 at 19:02):

Ok...

#### Johan Commelin (Apr 23 2019 at 19:02):

So in the lemma `Z`

is the "big type"?

#### Chris Hughes (Apr 23 2019 at 19:03):

Yes. Y is the adjoin_root and X is the algebraic closure

#### Chris Hughes (Apr 23 2019 at 19:03):

The definition isn't important, it's just an arbitrary map with that property defined with choice.

#### Johan Commelin (Apr 23 2019 at 19:04):

Right... that's what I figured now

#### Johan Commelin (Apr 23 2019 at 19:04):

In that case... I'm not sure if it will be used much outside of "Zorny" situations.

#### Johan Commelin (Apr 23 2019 at 19:05):

I would think it could even go in `algebraic_closure.zorn_aux`

:grinning:

Last updated: May 09 2021 at 09:11 UTC