Zulip Chat Archive

Stream: new members

Topic: partial functions and gluing


Jake Levinson (Sep 03 2021 at 05:34):

Hi all, I'm currently trying to do some basic point-set topology in Lean from the ground up -- partly to learn more about structures and typeclasses. I have looked a bit at topology in mathlib (only a little -- I kind of want to make my own mistakes, and I'm also not really fluent enough to read mathlib at length). I initially followed the first few section of Munkres Topology (open/closed sets, continuous functions).

I'm currently trying to formalize gluing, specifically gluing a fiber bundle given the data of a local trivialization.

The topology aspect is mostly all homeomorphisms. So the main challenge has really come from working with lots of subsets and/or subtypes and functions between them. I've read some discussions on here about it being generally preferable to use total functions with junk values. Would that be the right thing to do here? Or is there some way to make this easier?

For example, say π : E → B is a fiber bundle with fiber F and U : set B is a trivializing open set (i.e. I have the data of a bijection/homeomorphism φ : U × F → π ⁻¹' U). Then I find it surprisingly painful to show that any smaller subset U' ⊆ U is also trivializing. For example showing that φ restricted to U' × F maps to π ⁻¹' U' (and having to treat codomains similar to that one in two slightly different ways depending on whether they show up as a subtype of E or a subtype of π ⁻¹' U, i.e. a sub-subtype of E).

Here's my setup:

variables {E E' B : Type} {π : E  B} {π' : E'  B} {φ : E  E'}

lemma fiber_map_subset ( : π'  φ = π) {U : set B} {e : E} :
  e  π ⁻¹' U  φ e  π' ⁻¹' U :=
begin
  simp, rw [ function.comp_app π' φ, ],
end

def res_subset ( : π'  φ = π) (U : set B) : π ⁻¹' U  π' ⁻¹' U :=
  λ e, he⟩, φ e, (fiber_map_subset ).mp he

lemma fiber_map_inj_iff_res_inj ( : π'  φ = π) :
  function.injective φ 
   (U : set B), function.injective (res_subset  U) := sorry

lemma fiber_map_surj_iff_res_surj ( : π'  φ = π) :
  function.surjective φ 
   (U : set B), function.surjective (res_subset  U) := sorry

lemma fiber_map_bij_iff_res_bij ( : π'  φ = π) :
  function.bijective φ 
   (U : set B), function.bijective (res_subset  U) := sorry

For those, filling in the sorrys takes me about 5 lines each. But then proving the analogous iff statements for continuity and inverse-continuity and homeomorphisms takes me 60-70 lines. I won't copy that all here, but the lemma statement is:

-- I have defined a topology as a set of open sets
variables (TB : topology B) (TE : topology E) (TE' : topology E')

lemma fiber_map_cts_iff_res_cts
  (hπ_cts : cts TE TB π) (hπ'_cts : cts TE' TB π') ( : π'  φ = π) :
  topology.cts TE TE' φ 
   U (hU : U  TB.opens), cts TE TE' (res_subset  U) :=

-- proof of the above is 15-20 lines and uses:
def to_sub : set X  set A := λ U, {x : A | x.val  U}
def from_sub : set A  set X := λ U', {x : X |  hx : x  A, (⟨x, hx : A)  U'}
lemma to_sub_open_iff (U' : set A) :
  U'  (TX : topology A).opens   U  TX.opens, U' = to_sub A U := sorry
lemma from_sub_open_iff (hA : A  TX.opens) (U' : set A) :
  U'  (TX : topology A).opens  from_sub A U'  TX.opens := sorry

I'd be grateful for any comments or advice!

Johan Commelin (Sep 03 2021 at 06:34):

@Jake Levinson These issues are painful. Do you have a specific sorry that you want advice on?
One complication is that you seem to have built your own topology library, and I have no idea what exactly it looks like. So I have no idea whether those final two sorrys are supposed to be filled by iff.rfl, or that the definitions force you into a 20-line proof.

Reid Barton (Sep 03 2021 at 10:07):

Not sure if it will make things much easier, but I think it is better to work with open embeddings and not open subsets.

Reid Barton (Sep 03 2021 at 10:08):

For one thing, your mental picture of what is going on will be a lot closer to Lean's.

Jake Levinson (Sep 03 2021 at 15:53):

@Johan Commelin Hmm, thanks for the comments. Let me include a bit more of the code, though FWIW this gluing stuff is mostly independent of most earlier lemmas (which were on stuff like bases for a topology, interiors and closures, etc).

Here are two sorrys I would appreciate advice on.

  1. For the injectivity/bijectivity lemmas (which are purely about sets and functions, so no other lemmas necessary), I wonder if there is a way to get a one-line proof? For example I have:
lemma fiber_map_subset' ( : π'  φ = π) {U : set B} {e : E} :
  π e  U  π' (φ e)  U := by rw [ function.comp_app π' φ, ]

lemma fiber_map_surj_iff_res_surj ( : π'  φ = π) :
  function.surjective φ 
   (U : set B), function.surjective (res_subset  U) :=
begin
  split,
    rintros h U e', he'⟩,
    obtain e, he := h e',
    simp, exact e, by rwa [fiber_map_subset' , he], he⟩,
  intro h, specialize h set.univ,
  unfold function.surjective at h, simp at h, apply h,
end

This is reasonably short, going directly from the definition of surjectivity in both directions of the iff. (My first attempt was longer until I finally wrote the auxiliary lemma fiber_map_subset'). Still a little longer than I had expected.

  1. For fiber_map_cts_iff_res_cts (see below), I think my proof is pretty messy. Notably, I couldn't find an easy/clean way to deal with the distinction between functions E → E and {e : E // true} → {e : E // true} (this works OK in fiber_map_surj_iff_res_surj above via simp in the iff.mpr direction).

Here is my code, including my definitions of topology, continuous function, subspace topology (this should all be a working example, if not quite an #mwe):

import tactic
import data.set.basic

section topology

class topology (X : Type) :=
(opens : set (set X)) -- (should this instead be: is_open : set X → Prop ?)
(empty_open :   opens)
(univ_open : set.univ  opens)
(inter₂ :  (U V : set X), U  opens  V  opens  set.inter U V  opens)
(union :  (sU : set (set X)), sU  opens  ⋃₀ sU  opens)

variables {X Y : Type} (TX : topology X) (TY : topology Y) (f : X  Y)

def cts :=  V  TY.opens, f ⁻¹' V  TX.opens

instance inverse_image_topology : topology X := 
  {W : set X |  (U  TY.opens), W = f ⁻¹' U},
  , topology.empty_open, rfl⟩⟩,
  set.univ, topology.univ_open, rfl⟩⟩,
  sorry, -- written on the side
  sorry, -- written on the side


variable (A : set X)

instance subspace_topology : topology A :=
  inverse_image_topology TX (λ a, a.val)

instance topology_to_subspace_topology : has_coe (topology X) (topology A) :=
  λ TX, subspace_topology TX A

@[simp] def to_sub : set X  set A := λ U, {x : A | x.val  U}
@[simp] def from_sub : set A  set X := λ U', {x : X |  hx : x  A, (⟨x, hx : A)  U'}

-- Then I proved as many lemmas as I could think of about `to_sub` and `from_sub`. The only two I use below are:

lemma to_sub_open_iff (U' : set A) :
  U'  (TX : topology A).opens   U  TX.opens, U' = to_sub A U := sorry

lemma from_sub_open_iff (hA : A  TX.opens) (U' : set A) :
  U'  (TX : topology A).opens  from_sub A U'  TX.opens := sorry

end topology

-- Finally, here is `fiber_map_cts_iff_res_cts`.

section fiber_bundle

variables {E E' B : Type} {π : E  B} {π' : E'  B} {φ : E  E'}
  (TB : topology B) (TE : topology E) (TE' : topology E')

lemma fiber_map_subset ( : π'  φ = π) {U : set B} {e : E} :
  e  π ⁻¹' U  φ e  π' ⁻¹' U := by {simp, rw [ function.comp_app π' φ, ]}

lemma fiber_map_subset' ( : π'  φ = π) {U : set B} {e : E} :
  π e  U  π' (φ e)  U := by rw [ function.comp_app π' φ, ]

@[simp]
def res_subset ( : π'  φ = π) (U : set B) : π ⁻¹' U  π' ⁻¹' U :=
  λ e, he⟩, φ e, (fiber_map_subset ).mp he

lemma fiber_map_cts_iff_res_cts (hπ_cts : cts TE TB π) (hπ'_cts : cts TE' TB π') ( : π'  φ = π) :
  topology.cts TE TE' φ 
   U (hU : U  TB.opens), cts TE TE' (res_subset  U) :=
begin
  split,
  -- mp
  intros hφ_cts U hU V hV,
  let V_E' := from_sub _ V,
  have hV_E' := (from_sub_open_iff _ _ (hπ'_cts U hU) V).mp hV,
  specialize hφ_cts V_E' hV_E',
  have : res_subset  U ⁻¹' V = to_sub _ (φ ⁻¹' V_E'),
    ext e, he⟩, simp,
    rw fiber_map_subset  at he,
    split, intro h, exact he, h⟩, rintro h, h'⟩, exact h',
  rw [this, to_sub_open_iff],
  use (φ ⁻¹' V_E'), exact hφ_cts, rfl⟩,
  -- mpr
  intro hφU_cts,
  specialize hφU_cts set.univ TB.univ_open,
  intros V hV,
  specialize hφU_cts (to_sub set.univ V),
  rw to_sub_open_iff at hφU_cts, specialize hφU_cts V, hV, rfl⟩,
  rw from_sub_open_iff _ _ (hπ_cts _ TB.univ_open) at hφU_cts,
  convert hφU_cts,
  ext e, simp, refl,
end

end fiber_bundle

I have no idea if the above is even slightly readable, heh... and I found it very difficult to write. I would highlight that the mpr direction is quite complicated even though I have the hypothesis cts ↑TE ↑TE' (res_subset hφ set.univ), i.e. the restriction of φ to π ⁻¹' set.univ is continuous.

Jake Levinson (Sep 03 2021 at 15:57):

Reid Barton said:

Not sure if it will make things much easier, but I think it is better to work with open embeddings and not open subsets.

I considered doing this -- it definitely makes sense to me that there would be advantages to suppressing sets throughout and always replacing U : set X by f : U \to X and hf : open_immersion f.

I think my main hesitation was that I think I would then have to replace intersection of open sets by fiber product? I got the feeling that this approach would quickly lead me more towards formalizing category theory rather than topology, if that makes sense...

Kyle Miller (Sep 03 2021 at 16:02):

@Jake Levinson I started following along with your exercise last night to see to get a better idea of what you might be running into. I have exactly the same definition for topology (sets of sets seem fine to me). Here's a notation trick:

...
(opens [] : set (set X))
...

The square brackets make it take X explicitly, so you can write things like

lemma union_mem (U U' : set X) (h : U  opens X) (h' : U'  opens X) : U  U'  opens X

Kyle Miller (Sep 03 2021 at 16:04):

For inverse_image_topology, you don't want that to be an instance, since it depends on f and can't be used.

If you want to be terse for the definition of the open sets, you can do

def inverse_image_topology {α : Type w} (f : α  X) : topology α :=
{ opens := set.preimage f '' opens X,
   ... }

Kyle Miller (Sep 03 2021 at 16:05):

Once you have that, the subspace topology is

instance topology.subspace (s : set X) : topology s := inverse_image_topology (coe : s  X)

(coe is the official way to apply subtype.val)

Kyle Miller (Sep 03 2021 at 16:10):

For example, here's a short definition for from_sub:

def from_sub (A : set X) : set A  set X := set.image coe

and to_sub:

def to_sub (A : set X) : set X  set A := set.preimage coe

Kyle Miller (Sep 03 2021 at 16:13):

(I'm not sure I've used it yet, but these are related to another characterization of continuity:

lemma cts.def (f : X  Y) : cts f  set.preimage f '' opens Y  opens X

This is saying that set.image (set.preimage f) is the induced map on open sets.)

Kyle Miller (Sep 03 2021 at 16:16):

I find it somewhat more opaque to use set.image and set.preimage than just writing the sets out, but it's not so bad if you remind yourself what their underlying definitions are. The benefit is that you get to use whatever lemmas mathlib already has about these sets.

Jake Levinson (Sep 03 2021 at 23:13):

Kyle Miller said:

Jake Levinson I started following along with your exercise last night to see to get a better idea of what you might be running into. I have exactly the same definition for topology (sets of sets seem fine to me). Here's a notation trick:

...
(opens [] : set (set X))
...

The square brackets make it take X explicitly, so you can write things like

lemma union_mem (U U' : set X) (h : U  opens X) (h' : U'  opens X) : U  U'  opens X

Wow, this is fantastic! With that I was able to remove the implicit arguments from nearly everywhere. Thanks! One thing I still have to do is write U \in topology.opens X, not U \in opens X as you have. I'm not sure if there's some way to avoid that?

The other changes you suggested are quite helpful and I went and implemented them all. If you're curious, the repository is here -- https://github.com/mguaypaq/lean-topology. The stuff I posted here is in topology.lean and bundles.lean.

That said, my proof of fiber_map_cts_iff_res_cts remains long and messy.

Kyle Miller (Sep 03 2021 at 23:27):

To do opens by itself, either put the code in the topology namespace or do open topology. This makes all the names inside topology available without qualification.

Kyle Miller (Sep 03 2021 at 23:30):

The set-of-sets version of this is in data.set.lattice. There's a predicate on finiteness in data.set.finite that you could use when you want to do just finite intersections (so if s is a set, (h : s.finite) would be how you indicate that you need a proof of finiteness)

Kyle Miller (Sep 03 2021 at 23:30):

Oh, I misunderstood what you are doing

Kyle Miller (Sep 03 2021 at 23:31):

It tends to be frowned upon overloading notation without using a typeclass, like has_add etc.)

Kyle Miller (Sep 03 2021 at 23:39):

For example, this could be open_of_inter_of_finset:

lemma sInter_mem (sU : set (set X)) (hf : sU.finite) (h : sU  topology.opens X) :
  ⋂₀ sU  topology.opens X :=
begin
  refine set.finite.induction_on hf _ _ h, -- the h at the end effectively adds h as an additional induction hypothesis
  -- this would be clearer:
  --   revert h,
  --   refine set.finite.induction_on hf _ _,
  { intro _,
    simp [univ_mem], },
  { intros U sU' hU hf h hi,
    rw set.sInter_insert,
    rw set.insert_subset at hi,
    apply inter_mem,
    { exact hi.1 },
    { apply h,
      exact hi.2, }, },
end

Kyle Miller (Sep 03 2021 at 23:43):

(This also saves you from needing to worry about decidable equality.)

Jake Levinson (Sep 04 2021 at 00:16):

That's interesting, I did find the whole decidable-equality thing confusing. (I haven't actually used those finite-intersection lemmas elsewhere -- I just proved them early on, so they're at the top of the file.) I'll try to understand your solution.

Incidentally -- the topology.lean file is super long since I just kept adding to it as I went. I guess it's probably better to split it into several smaller files at some point. (For instance the sections on interiors and closures, on continuous functions, on bases, on product and subspace topologies, etc).

Jake Levinson (Sep 04 2021 at 00:21):

I wonder if the from_sub and to_sub lemmas can now all be removed to work directly with properties of set.image and set.preimage and coe. I tried doing this a little bit. I was surprised by how annoying those fiber_map lemmas were to prove.


Last updated: Dec 20 2023 at 11:08 UTC