Covering Spaces

Stream: Berkeley Lean Seminar

[Thomas Browning]

@Jordan Brown I refactored the definition of covering space (branch#covering). I think that it might be helpful to have both a structure with data (even_covering) and a predicate (evenly_covered). The structure with data is useful for explicit constructions (e.g., translate). The predicate is useful for higher-level stuff (e.g., covering_map). You will need to git pull to get the new definition.

[Thomas Browning]

@Jordan Brown An interesting question: Currently we are asserting a homeomorphism f ⁻¹' {x} × U ≃ₜ f ⁻¹' U compatible with mapping to U. Do we also want to assert compatibility with mapping from f ⁻¹' {x}? This is a sort of rigidity property that prevents permutation of f ⁻¹' {x}.

[Thomas Browning]

If the fibers are discrete, then compatibility with f ⁻¹' {x} can be achieved by permutation. So the question is just whether we want to impose compatibility with f ⁻¹' {x} when the fibers are not discrete. (Is there a nice example of non-discrete fibers?)

[Thomas Browning]

I guess the obvious example is I × U for I not discrete.

[Filippo A. E. Nuccio]

@Thomas Browning Are you aware of @Shing Tak Lam 's branch on covering spaces?

[Shing Tak Lam]

(I didn't do much on that branch so I wouldn't really bother with looking at it)

[Filippo A. E. Nuccio]

BTW: Are you still working on homotopy-related stuff? Because during summer I wanted to start looking a bit into $\pi_1$ on my spare time, and would like to avoid stepping on anyone's toes.

[Shing Tak Lam]

Not really, I have a few other things going on so I wouldn't worry about what I'm doing.

[Kevin Buzzard]

I thought that we had pi_1 and were well on the way to pi_n by now? But you mean the relation with covering spaces? That would be cool.

[Thomas Browning]

I think @Jordan Brown wants to get to the relation between fundamental groups and covering spaces.

[Kevin Buzzard]

yeah that would be a really cool thing to have.

[Filippo A. E. Nuccio]

AFAIK we only have the type $\pi_1$ but not yet that it is a group, no?

[Johan Commelin]

What is the mathlib name? Then you can ask the docs which instances it carries, right?

[Adam Topaz]

I think it's a group (according to mathlib)

[Adam Topaz]

IIRC we even have the fundamental groupoid

[Adam Topaz]

docs#fundamental_group docs#fundamental_groupoid

[Filippo A. E. Nuccio]

Oh sure, I was thinking about the version with paths and homotopies in topology/homotopy.

[Adam Topaz]

I'm not sure what you mean.... the fundamental groupoid is the groupoid whose objects are the points of X and whose morphisms are homotopy equivalences of paths

[Adam Topaz]

do we have two versions of the fundamental group?

[Filippo A. E. Nuccio]

I have #14724 in mind

[Adam Topaz]

Ah I see, that's $\pi_n$

[Adam Topaz]

I would have expected to use iterated loop-spaces and $\pi_0$ to construct this

[Thomas Browning]

I opened a pull request with the definition: #15276

[Thomas Browning]

example {X : Type*} [topological_space X] (s t : set X) (hs : is_open s) (h : is_open ((coe : s → X) ⁻¹' t)) :
  is_open (t ∩ s) :=
begin
  rw [inducing.is_open_iff (inducing_coe)] at h,
  obtain ⟨a, b, c⟩ := h,
  rw [subtype.preimage_coe_eq_preimage_coe_iff] at c,
  rw ← c,
  exact is_open.inter b hs,
end

[Jordan Brown]

lemma induced_topology (Y:Type*) [topological_space Y] (A: set Y)
(hA: ∀ x:Y, ∃ (U : set Y) (hU : U ∈ 𝓝 x), is_open ((coe : U → Y)⁻¹' A)):is_open A

[Thomas Browning]

lemma induced_topology (Y:Type*) [topological_space Y] (A: set Y)
(hA: ∀ x:Y, ∃ (U : set Y) (hU : U ∈ 𝓝 x), is_open ((coe : U → Y)⁻¹' A)):is_open A :=
is_open_iff_forall_mem_open.mpr (λ x hx, let ⟨U, hU1, hU2⟩ := hA x,
  ⟨V, hV1, hV2, hV3⟩ := mem_nhds_iff.mp hU1 in ⟨A ∩ V, set.inter_subset_left A V,
    mylem V A hV2 ((continuous_inclusion hV1).is_open_preimage _ hU2), hx, hV3⟩)

[Thomas Browning]

lemma mylem {X : Type*} [topological_space X] (s t : set X) (hs : is_open s)
  (h : is_open ((coe : s → X) ⁻¹' t)) : is_open (t ∩ s) :=
let ⟨a, b, c⟩ := inducing_coe.is_open_iff.mp h in
  subtype.preimage_coe_eq_preimage_coe_iff.mp c ▸ b.inter hs

[Thomas Browning]

@Jordan Brown If you haven't proved it yourself yet, here's a rather unpolished proof of key:

      have key : ∀ y : d, f₁ y = f₂ y ↔ g₁ y = g₂ y,
      { refine λ y, ⟨congr_arg (prod.snd ∘ c.1), _⟩,
        intro m,
        have h0 : f (f₁ y) = f (f₂ y) := congr_fun h y,
        refine c.inj_on (c.mem_source.mpr y.2) (c.mem_source.mpr (h0 ▸ y.2)) _,
        have ha : f (f₁ y) ∈ c.base_set := y.2,
        have hb : f (f₂ y) ∈ c.base_set := h0 ▸ y.2,
        change c (f₁ y) = c (f₂ y),
        refine prod.ext _ m,
        rwa [c.coe_fst', c.coe_fst'],
        rw ← h0,
        exact y.2,
        exact y.2, },

[Jordan Brown]

excellent, I had not finished the proof

[Jordan Brown]

(what does the triangle do?)

[Johan Commelin]

It is basically a term-mode version of rw.