Initial topology induced by a family of functions

[mkerjean]

Motivation for this change

Enhances initial_topoly.v by constructing the topology induced by a family of functions, instead of a single one.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[mkerjean]

The CI is red, and I do not understand why (is it a Nix error ?). Lemma https://github.com/mkerjean/analysis/blob/47c3e604894453fcad960c298b127a3d813c3aed/theories/topology_theory/initial_topology.v#L362 (https://github.com/mkerjean/analysis/blob/47c3e604894453fcad960c298b127a3d813c3aed/theories/topology_theory/initial_topology.v#L362) is said not to compile while the whole library compiles on my computer. Can someone help me understand what's going on? This is a small PR, and I would prefer not to let it gather dust for too long.

[zstone1]

Note that I have used sup_topology for this sometimes, as in completely_regular_uniformity. I am pretty sure its the construction you want.

Im definitely happy to have "initial for multiple functions at once" be more ergonomic, so glad to see this PR. But mostly wanted to highlight this alternative definition. It might make some proofs factor better using the existing machinery, E.G. like uniform structure for sup topology for free.

[mkerjean]

Note that I have used sup_topology for this sometimes, as in completely_regular_uniformity. I am pretty sure its the construction you want.

Im definitely happy to have "initial for multiple functions at once" be more ergonomic, so glad to see this PR. But mostly wanted to highlight this alternative definition. It might make some proofs factor better using the existing machinery, E.G. like uniform structure for sup topology for free.

Oh yes, I overlooked that, of course, sup + initial is initial_fam. Not sure this PR is necessary then, maybe just a documentation issue. I've also refined one lemma about initial topology (cvg_image has become cvg_initial and cvg_image and continuous_initial have been added to get rid of the hypothesis about the surjectivity of the function). Maybe the PR can be reduced to these lemmas + an indication in the header on how to define the initial topology for a family of functions.

[mkerjean]

Note that I have used sup_topology for this sometimes, as in completely_regular_uniformity. I am pretty sure its the construction you want.

Im definitely happy to have "initial for multiple functions at once" be more ergonomic, so glad to see this PR. But mostly wanted to highlight this alternative definition. It might make some proofs factor better using the existing machinery, E.G. like uniform structure for sup topology for free.

Looking more in detail at the use of sup, it seems that the composition of initial_topology and sup_topolgy isn't satisfactory. If I understand well, you're suggesting a definition as follows :

Section initial_fam_Topology_with_sup.
Variable (S : choiceType)  (I : pointedType) (T : I -> topologicalType)  (F : forall i :I, (S -> T i)).

Definition Fc := fun i => Topological.class (initial_topology (F i)).

Definition initial_sup_topology := (sup_topology Fc).

but then, when (T : I -> Uniform.Type), one can´t build an instance of a uniform_type on initial_sup_topoly due to the use of Topological.class. One would need to define both initial_sup_uniform and initial_sup_topology. Do you see a workaround @zstone1 ? Or did you have something else in mind?

Note that now there is an instance of a uniform type on initial_fam_topology (with one admit I can't get rid of at the moment).