How to wisely state Homotopy lifting lemma

Stream: Is there code for X?

[Ruize Chen]

I am trying to formalise the fact that there is an isomorphism between fundamental group of a circle and integer. So I need to use this lemma. However, I cannot find the definition of lifting (the lifting working with covering space). So I have made one

variable {Y : Type} [TopologicalSpace Y]
variable {X : Type} [TopologicalSpace X]
variable {E : Type} [TopologicalSpace E]

variable (f₁ : C(Y, X)) (f₂ : C(Y, X)) (h_homo: ContinuousMap.Homotopic f₁ f₂)

variable (homo_lift: f₁.Homotopy f₂)

variable (f : C(Y, X))
variable (p : E → X) (hc: IsCoveringMap p)

@[ext]
structure lift_AT where
  f_lift : C(Y, E)
  hlift_1 : f = p ∘ f_lift

variable (lf₁ : lift_AT f₁ p)

I also put some of the defined functions for the homotopy lifting lemma above. Then I started to try to state the lemma. I am not familiar with the use of homotopy yet, but I am sure that I might not be using it correctly by mentioning the homotopic statement and the homotopy function at the same time (I feel like homotopic implies the existence of homotopy). For the lift of homotpy, I made this attempt:

@[ext]
structure lift_HT where
  f_lift : C(↑unitInterval × Y, E)
  hlift : homo_lift = p ∘ f_lift

#check lift_HT f₁ f₂ homo_lift p

I think the lemma is about showing the existence of this thing and the uniqueness. My question is, how can I input this lemma in a good way, is it necessary to define another lift for homotopy?

[Johan Commelin]

cc @Junyan Xu who recently worked on adjacent material in mathlib

[Ruize Chen]

theorem Homotopy_lifting_lemma_unique (H₁ H₂ : lift_HT f₁ f₂ homo_lift p): H₁ = H₂:= by
  sorry

theorem Homotopy_lifting_lemma_ext: Nonempty (lift_HT f₁ f₂ homo_lift p) := by
  sorry

I think this might be the one.

[Junyan Xu]

I think I'd aim for the more general result that if one has a free and properly discontinuous action of a group G on a topological space X, then one gets a covering map (#7596) X → X / G that is Galois (i.e. the range of the induced map between fundamental groups is a normal subgroup; it's known from #22649 that the map is injective). Using the mechanism of monodromy in #22771 we should be able to show that G is isomorphic to the quotient $\pi_1(X/G)/\pi_1(X)$. Now if X is the real line and G is the subgroup of integers, then X/G is the circle and $\pi_1(X)=1$, so we get the isomorphism $\pi_1(X/G)\cong G\cong\mathbb{Z}$. Notice that #7596 doesn't require the target to be X/G and can work with any quotient map.