Commit 2023-01-30 21:46 bcfa7268

refactor(topology/{order,*}): review API (#18312)

Main changes

• Switch from @[class] structure topological_space to class.
• Introduce notation is_open[t]/is_closed[t]/𝓤[u] and use it instead of t.is_open/@is_closed _ t/u.uniformity
• Don't introduce a temporary order on topological_space, use galois_coinsertion to the order-dual of set (set α) instead.
• Drop discrete_topology_bot. It seems that this instance doesn't work well in Lean 4 (in fact, I failed to define it without using @DiscreteTopology.mk).

Other changes

Topological spaces

• Add is_open_mk.
• Rename generate_from_mono to generate_from_anti, move it to the topological_space namespace.
• Add embedding_inclusion, embedding_ulift_down, and ulift.discrete_topology.
• Move discrete_topology.of_subset from topology.separation to topology.constructions.
• Move embedding.discrete_topology from topology.separation to topology.maps.
• Use explicit arguments in an argument of nhds_mk_of_nhds.
• Move some definitions and lemmas like mk_of_closure, gi_generate_from (renamed to gci_generate_from), left_inverse_generate_from to the topological_space namespace. These lemmas are very specific and use generic names.
• Add topological_space and discrete_topology instances for fin n.
• Drop is_open_induced_iff', use non-primed version instead.
• Prove set_of_is_open_sup by rfl.
• Drop nhds_bot, use nhds_discrete instead.
• Drop induced_bot and discrete_topology_induced

Uniform spaces

• Drop infi_uniformity' and inf_uniformity'.
• Use @uniformity α (uniform_space.comap _ _) instead of (h : ‹uniform_space α› = uniform_space.comap f ‹uniform_space β›) in uniformity_comap.

Locally constant functions and discrete quotients

• Use quotient space topology for the coercion of a discrete_quotient to Type*, then prove [discrete_topology]. This way we avoid surprising diamonds in the future (especially if Lean 4 will unfold the coercion).
• Merge locally_constant.lift and locally_constant.locally_constant_lift into 1 def, rename factors to lift_comp_proj.
• Protect locally_constant.is_locally_constant.
• Drop locally_constant.iff_continuous_bot

Categories

• Add an instance for discrete_topology (discrete.obj X).
• Rename Fintype.discrete_topology to Fintype.bot_topology , add lemma Fintype.discrete_topology sating that this is a [discrete_topology].

Topological rings

• Fix&golf a proof that failed because of API changes.