bundles

Stream: maths

[Floris van Doorn]

What should be the simp-normal form of the map bundle.total_space E -> B?
Currently it is docs#sigma.fst since docs#bundle.proj simplifies to sigma.fst. However, if sigma.fst, why do we even define bundle.proj in the first place? If sigma.fst is simp-normal form, we want to use sigma.fst everywhere, and not bundle.proj.

[Floris van Doorn]

@Nicolò Cavalleri

[Eric Wieser]

There might be some discussion about that in #4658 which introduced it

[Eric Wieser]

My guess would be that it exists for dot notation, but is removed by simp to avoid repeating tonnes of boring lemmas

[Eric Wieser]

Tangential question; why does docs#bundle seem to pick up instances for other types of bundle?

[Eric Wieser]

Are those other bundle types deliberately marked as reducible?

[Sebastien Gouezel]

Floris van Doorn said:

What should be the simp-normal form of the map bundle.total_space E -> B?
Currently it is docs#sigma.fst since docs#bundle.proj simplifies to sigma.fst. However, if sigma.fst, why do we even define bundle.proj in the first place? If sigma.fst is simp-normal form, we want to use sigma.fst everywhere, and not bundle.proj.

To me, this question is related to type synonyms. sigma.fst goes from Σ x, E x to B, while bundle.proj E goes from total_space E to B. Since these two spaces don't have the same typeclasses, I think it really makes a difference when discussing, say, continuity of the projection, as the topologies on Σ x, E x and total_space E are typically not the same. But writing v.1 is much more convenient than writing proj E v, so I have mixed feelings.

[Kyle Miller]

Would it be a bad idea to make E implicit for proj? Then you could write v.proj instead of proj E v. When you just want the projection map you might need @proj _ foo though for a specific bundle foo (which in Lean 4 you'll be able to write as proj (E := foo)).

Without making it implicit, I think v.proj _ should work, but there are occasions where you need to put parentheses around the whole expression.

[Sebastien Gouezel]

I think that's a good idea, since the @ version is not too verbose.

[Floris van Doorn]

I had similar concerns to those of Sebastien: if we write a type synonym, we should develop and use its API. I like the suggestion to make the argument E of proj implicit. I will PR that.

[Floris van Doorn]

#14359