What is the second output of PartialHomeomorph

Stream: Is there code for X?

[Ruize Chen]

I am trying to prove that if f_1 and f_2 are both lifts of function f from Topological space Y (connected)to Topological space X, then they agree everywhere or nowhere. In the proof I need to use the evenly covered property and by rewriting things I got the homomorphism. In lean it's PartialHomeomorph. I suppose I need to use injectivity to do this part:

Indeed, by construction \[ p_{| \bar{U}} \circ \tilde{f}_1 |_{V} = p_{| \bar{U}} \circ \tilde{f}_2 |_{V}. \] Since \( p_{| \bar{U}} \) is a homeomorphism, it follows that \[ \tilde{f}_1 |_{V} = \tilde{f}_2 |_{V}. \]

However, I can only prove that (↑ph (f₁.f_lift v)).1 = (↑ph (f₂.f_lift v)).1 since the condition I have is ∀ p_1 ∈ ph.source, (↑ph p_1).1 = p p_1. When it comes to proving (↑ph (f₁.f_lift v)).2 = (↑ph (f₂.f_lift v)).2, I didn't find any conditions obtained with PartialHomeomorph related to this second output.
So my question is: what second output, how is it defined? Or am I using the correct way (PartialHomeomorph.injOn) to prove it?

[Ruize Chen]

sorry the latex is not looking good I just put a screenshot of the proof
image.png

[Ruize Chen]

And the whole thing (PartialHomeomorph and the related conditions ) comes from the structure Trivialization

ph : PartialHomeomorph E (X × ↑(p ⁻¹' {x}))
U : Set X
hU : IsOpen U
hU2 : ph.source = p ⁻¹' U
hU3 : ph.target = U ×ˢ Set.univ
hp2 : ∀ p_1 ∈ ph.source, (↑ph p_1).1 = p p_1

[Bhavik Mehta]

Hi Ruize, glad to see you made it here! The output of PartialHomeomorph here is in the type X × ↑(p ⁻¹' {x}), which is a product type. So the second output is something of type ↑(p ⁻¹' {x}), ie an element of this fibre

[Bhavik Mehta]

(In the future, you'll get more luck getting help if you post questions as #mwe: in this case you got lucky that I know what you are working on so I could figure it out!)

[Ruize Chen]

yeah fiber it is, but I didn't see any thing defined about this, I believe if I need to use injectivity, I have to find how it's defined, (I feel like I have done the main proof, I think the second element provides some trivial info) yet I didn't find a way to rewrite it

[Ruize Chen]

Bhavik Mehta said:

(In the future, you'll get more luck getting help if you post questions as #mwe: in this case you got lucky that I know what you are working on so I could figure it out!)

thank you for the tip, and staying up this late

[Bhavik Mehta]

There won't be anything defined about this in PartialHomeomorph in general (that might not have a second component whatsoever), you'll need to get this fact from the local context you have

[Ruize Chen]

I feel like the thing i have should give me a homeomorphism, (yeah it's there called PartialHomeomorph), with similar things (the first component works just like a homeomorphism) . I am confused about the fact that I didn't find anything similar in the proof. If the thing is related to the local context, how should I deal with the target (↑ph (f₁.f_lift v)).2 = (↑ph (f₂.f_lift v)).2, is there any tactics

[Ruize Chen]

Probably things will be clear in the problem class, or when I meet you or TAs. I think it's not a big issue, it's the only sorry in my first half (proof of openset). My brain might not be working properly at this moment. I might try rw some conditions that are not used (I think that might be the local context you implied
)

[Bhavik Mehta]

Yup, best thing to do here is to show somebody some more code: either that means seeing me or TAs on Thursday or posting a #mwe here

[Winston Yin (尹維晨)]

Hi Ruize, you could put double dollar signs around your LaTeX so it’s easier to read on Zulip!