What is this lemma called?

Stream: maths

[Chris Hughes]

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]

Your def seems incomplete...

[Chris Hughes]

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

[Chris Hughes]

Or an injective map with that property.

[Johan Commelin]

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

[Chris Hughes]

Yes

[Johan Commelin]

Also... where does your map come up in practice? I don't really understand what's going on...

[Chris Hughes]

It came up doing algebraic closure.

[Johan Commelin]

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

[Chris Hughes]

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]

Doing zorn on this gives the algebraic closure.

[Chris Hughes]

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]

Ok...

[Johan Commelin]

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

[Chris Hughes]

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

[Chris Hughes]

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

[Johan Commelin]

Right... that's what I figured now

[Johan Commelin]

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

[Johan Commelin]

I would think it could even go in algebraic_closure.zorn_aux :grinning: