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

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

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