Zulip Chat Archive

Stream: Berkeley Lean Seminar

Topic: Covering Spaces


Thomas Browning (Jul 01 2022 at 22:27):

@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 (Jul 02 2022 at 00:38):

@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 (Jul 02 2022 at 01:42):

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 (Jul 02 2022 at 02:04):

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

Filippo A. E. Nuccio (Jul 04 2022 at 12:53):

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

Shing Tak Lam (Jul 04 2022 at 12:56):

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

Filippo A. E. Nuccio (Jul 04 2022 at 13:05):

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

Shing Tak Lam (Jul 04 2022 at 15:00):

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

Kevin Buzzard (Jul 04 2022 at 16:15):

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 (Jul 04 2022 at 21:16):

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

Kevin Buzzard (Jul 04 2022 at 22:14):

yeah that would be a really cool thing to have.

Filippo A. E. Nuccio (Jul 05 2022 at 12:31):

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

Johan Commelin (Jul 05 2022 at 12:42):

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

Adam Topaz (Jul 05 2022 at 12:53):

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

Adam Topaz (Jul 05 2022 at 12:53):

IIRC we even have the fundamental groupoid

Adam Topaz (Jul 05 2022 at 12:54):

docs#fundamental_group docs#fundamental_groupoid

Filippo A. E. Nuccio (Jul 05 2022 at 12:56):

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

Adam Topaz (Jul 05 2022 at 12:58):

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 (Jul 05 2022 at 12:59):

do we have two versions of the fundamental group?

Filippo A. E. Nuccio (Jul 05 2022 at 13:01):

I have #14724 in mind

Adam Topaz (Jul 05 2022 at 13:05):

Ah I see, that's πn\pi_n

Adam Topaz (Jul 05 2022 at 13:07):

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

Thomas Browning (Jul 12 2022 at 15:58):

I opened a pull request with the definition: #15276

Thomas Browning (Oct 14 2022 at 00:03):

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 (Oct 20 2022 at 22:12):

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 (Oct 20 2022 at 22:26):

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 (Oct 20 2022 at 22:30):

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 (Apr 17 2023 at 23:53):

@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 (Apr 18 2023 at 05:44):

excellent, I had not finished the proof

Jordan Brown (Apr 18 2023 at 05:45):

(what does the triangle do?)

Johan Commelin (Apr 18 2023 at 05:57):

It is basically a term-mode version of rw.


Last updated: Dec 20 2023 at 11:08 UTC