partial functions and gluing

Stream: new members

[Jake Levinson]

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 (hφ : π' ∘ φ = π) {U : set B} {e : E} :
  e ∈ π ⁻¹' U ↔ φ e ∈ π' ⁻¹' U :=
begin
  simp, rw [← function.comp_app π' φ, hφ],
end

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

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

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

lemma fiber_map_bij_iff_res_bij (hφ : π' ∘ φ = π) :
  function.bijective φ ↔
  ∀ (U : set B), function.bijective (res_subset hφ 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 π') (hφ : π' ∘ φ = π) :
  topology.cts TE TE' φ ↔
  ∀ U (hU : U ∈ TB.opens), cts ↑TE ↑TE' (res_subset hφ 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]

@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]

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]

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

[Jake Levinson]

@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' (hφ : π' ∘ φ = π) {U : set B} {e : E} :
  π e ∈ U ↔ π' (φ e) ∈ U := by rw [← function.comp_app π' φ, hφ]

lemma fiber_map_surj_iff_res_surj (hφ : π' ∘ φ = π) :
  function.surjective φ ↔
  ∀ (U : set B), function.surjective (res_subset hφ U) :=
begin
  split,
    rintros h U ⟨e', he'⟩,
    obtain ⟨e, he⟩ := h e',
    simp, exact ⟨e, by rwa [fiber_map_subset' hφ, 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.

2. 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 (hφ : π' ∘ φ = π) {U : set B} {e : E} :
  e ∈ π ⁻¹' U ↔ φ e ∈ π' ⁻¹' U := by {simp, rw [← function.comp_app π' φ, hφ]}

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

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

lemma fiber_map_cts_iff_res_cts (hπ_cts : cts TE TB π) (hπ'_cts : cts TE' TB π') (hφ : π' ∘ φ = π) :
  topology.cts TE TE' φ ↔
  ∀ U (hU : U ∈ TB.opens), cts ↑TE ↑TE' (res_subset hφ 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 hφ U ⁻¹' V = to_sub _ (φ ⁻¹' V_E'),
    ext ⟨e, he⟩, simp,
    rw fiber_map_subset hφ 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]

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]

@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]

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]

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]

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]

(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]

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]

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]

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]

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]

Oh, I misunderstood what you are doing

[Kyle Miller]

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

[Kyle Miller]

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]

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

[Jake Levinson]

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]

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.