Zulip Chat Archive

Stream: maths

Topic: What is this lemma called?


view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 23 2019 at 18:54):

Your def seems incomplete...

view this post on Zulip Chris Hughes (Apr 23 2019 at 18:55):

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

view this post on Zulip Chris Hughes (Apr 23 2019 at 18:56):

Or an injective map with that property.

view this post on Zulip Johan Commelin (Apr 23 2019 at 18:57):

Is embedding.trans what I would have called embedding.comp?

view this post on Zulip Chris Hughes (Apr 23 2019 at 18:58):

Yes

view this post on Zulip 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...

view this post on Zulip Chris Hughes (Apr 23 2019 at 18:58):

It came up doing algebraic closure.

view this post on Zulip Johan Commelin (Apr 23 2019 at 18:59):

Would you mind copy-pasting the entire definition of map? And more context if you want?

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Apr 23 2019 at 19:00):

Doing zorn on this gives the algebraic closure.

view this post on Zulip 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".

view this post on Zulip Johan Commelin (Apr 23 2019 at 19:02):

Ok...

view this post on Zulip Johan Commelin (Apr 23 2019 at 19:02):

So in the lemma Z is the "big type"?

view this post on Zulip Chris Hughes (Apr 23 2019 at 19:03):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 23 2019 at 19:04):

Right... that's what I figured now

view this post on Zulip 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.

view this post on Zulip 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