This file defines homeomorphisms between open subsets of topological spaces. An element e of local_homeomorph α β is an extension of local_equiv α β, i.e., it is a pair of functions e.to_fun and e.inv_fun, inverse of each other on the sets e.source and e.target. Additionally, we require that these sets are open, and that the functions are continuous on them. Equivalently, they are homeomorphisms there.
Contrary to equivs, we do not register the coercion to functions and we use explicitly to_fun and inv_fun: coercions create unification problems for manifolds.
homeomorph.to_local_homeomorph: associating a local homeomorphism to a homeomorphism, with source = target = univ local_homeomorph.symm : the inverse of a local homeomorphism local_homeomorph.trans : the composition of two local homeomorphisms local_homeomorph.refl : the identity local homeomorphism local_homeomorph.of_set: the identity on a set s eq_on_source : equivalence relation describing the "right" notion of equality for local homeomorphisms
Most statements are copied from their local_equiv versions, although some care is required especially when restricting to subsets, as these should be open subsets.
For design notes, see local_equiv.lean.
local homeomorphisms, defined on open subsets of the space
A homeomorphism induces a local homeomorphism on the whole space
Two local homeomorphisms are equal when they have equal to_fun, inv_fun and source. It is not sufficient to have equal to_fun and source, as this only determines inv_fun on the target. This would only be true for a weaker notion of equality, arguably the right one, called eq_on_source.
The inverse of a local homeomorphism
A local homeomorphism is continuous at any point of its source
A local homeomorphism inverse is continuous at any point of its target
Preimage of interior or interior of preimage coincide for local homeomorphisms, when restricted to the source.
The image of an open set in the source is open.
Restricting a local homeomorphism e to e.source ∩ s when s is open. This is sometimes hard to use because of the openness assumption, but it has the advantage that when it can be used then its local_equiv is defeq to local_equiv.restr
Restricting a local homeomorphism e to e.source ∩ interior s. We use the interior to make sure that the restriction is well defined whatever the set s, since local homeomorphisms are by definition defined on open sets. In applications where s is open, this coincides with the restriction of local equivalences
The identity on the whole space as a local homeomorphism.
The identity local equiv on a set s
Composition of two local homeomorphisms when the target of the first and the source of the second coincide.
Composing two local homeomorphisms, by restricting to the maximal domain where their composition is well defined.
eq_on_source e e' means that e and e' have the same source, and coincide there. They should really be considered the same local equiv.
eq_on_source is an equivalence relation
If two local homeomorphisms are equivalent, so are their inverses
Two equivalent local homeomorphisms have the same source
Two equivalent local homeomorphisms have the same target
Two equivalent local homeomorphisms have coinciding to_fun on the source
Two equivalent local homeomorphisms have coinciding inv_fun on the target
Composition of local homeomorphisms respects equivalence
Restriction of local homeomorphisms respects equivalence
Composition of a local homeomorphism and its inverse is equivalent to the restriction of the identity to the source
The product of two local homeomorphisms, as a local homeomorphism on the product space.
Continuity within a set at a point can be read under right composition with a local homeomorphism, if the point is in its target
Continuity at a point can be read under right composition with a local homeomorphism, if the point is in its target
A function is continuous on a set if and only if its composition with a local homeomorphism on the right is continuous on the corresponding set.
Continuity within a set at a point can be read under left composition with a local homeomorphism if a neighborhood of the initial point is sent to the source of the local homeomorphism
Continuity at a point can be read under left composition with a local homeomorphism if a neighborhood of the initial point is sent to the source of the local homeomorphism
A function is continuous on a set if and only if its composition with a local homeomorphism on the left is continuous on the corresponding set.
If a local homeomorphism has source and target equal to univ, then it induces a homeomorphism between the whole spaces, expressed in this definition.