Local equivalences
This files defines equivalences between subsets of given types.
An element e of local_equiv α β is made of two maps e.to_fun and e.inv_fun respectively
from α to β and from β to α (just like equivs), which are inverse to each other on the subsets
e.source and e.target of respectively α and β.
They are designed in particular to define charts on manifolds.
The main functionality is e.trans f, which composes the two local equivalences by restricting
the source and target to the maximal set where the composition makes sense.
As for equivs, we register a coercion to functions and use it in our simp normal form: we write
e x and e.symm y instead of e.to_fun x and e.inv_fun y.
Main definitions
equiv.to_local_equiv: associating a local equiv to an equiv, with source = target = univ
local_equiv.symm : the inverse of a local equiv
local_equiv.trans : the composition of two local equivs
local_equiv.refl : the identity local equiv
local_equiv.of_set : the identity on a set s
eq_on_source : equivalence relation describing the "right" notion of equality for local
equivs (see below in implementation notes)
Implementation notes
There are at least three possible implementations of local equivalences:
- equivs on subtypes
- pairs of functions taking values in
option αandoption β, equal to none where the local equivalence is not defined - pairs of functions defined everywhere, keeping the source and target as additional data
Each of these implementations has pros and cons.
- When dealing with subtypes, one still need to define additional API for composition and
restriction of domains. Checking that one always belongs to the right subtype makes things very
tedious, and leads quickly to DTT hell (as the subtype
u ∩ vis not the "same" asv ∩ u, for instance). - With option-valued functions, the composition is very neat (it is just the usual composition, and
the domain is restricted automatically). These are implemented in
pequiv.lean. For manifolds, where one wants to discuss thoroughly the smoothness of the maps, this creates however a lot of overhead as one would need to extend all classes of smoothness to option-valued maps. - The local_equiv version as explained above is easier to use for manifolds. The drawback is that
there is extra useless data (the values of
to_funandinv_funoutside ofsourceandtarget). In particular, the equality notion between local equivs is not "the right one", i.e., coinciding source and target and equality there. Moreover, there are no local equivs in this sense between an empty type and a nonempty type. Since empty types are not that useful, and since one almost never needs to talk about equal local equivs, this is not an issue in practice. Still, we introduce an equivalence relationeq_on_sourcethat captures this right notion of equality, and show that many properties are invariant under this equivalence relation.
A very basic tactic to show that sets showing up in manifolds coincide or are included in one another.
- to_fun : α → β
- inv_fun : β → α
- source : set α
- target : set β
- map_source' : ∀ {x : α}, x ∈ c.source → c.to_fun x ∈ c.target
- map_target' : ∀ {x : β}, x ∈ c.target → c.inv_fun x ∈ c.source
- left_inv' : ∀ {x : α}, x ∈ c.source → c.inv_fun (c.to_fun x) = x
- right_inv' : ∀ {x : β}, x ∈ c.target → c.to_fun (c.inv_fun x) = x
Local equivalence between subsets source and target of α and β respectively. The (global)
maps to_fun : α → β and inv_fun : β → α map source to target and conversely, and are inverse
to each other there. The values of to_fun outside of source and of inv_fun outside of target
are irrelevant.
Associating a local_equiv to an equiv
Equations
- e.to_local_equiv = {to_fun := e.to_fun, inv_fun := e.inv_fun, source := set.univ α, target := set.univ β, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}
The inverse of a local equiv
Equations
- e.symm = {to_fun := e.inv_fun, inv_fun := e.to_fun, source := e.target, target := e.source, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}
Equations
- local_equiv.has_coe_to_fun = {F := λ (x : local_equiv α β), α → β, coe := local_equiv.to_fun β}
Associating to a local_equiv an equiv between the source and the target
A local equiv induces a bijection between its source and target
Restricting a local equivalence to e.source ∩ s
The identity local equiv
Equations
The identity local equiv on a set s
Equations
- local_equiv.of_set s = {to_fun := id α, inv_fun := id α, source := s, target := s, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}
Composing two local equivs if the target of the first coincides with the source of the second.
Composing two local equivs, 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. Then e
and e' should really be considered the same local equiv.
eq_on_source is an equivalence relation
Equations
- local_equiv.eq_on_source_setoid = {r := local_equiv.eq_on_source β, iseqv := _}
Two equivalent local equivs have the same source
Two equivalent local equivs coincide on the source
Two equivalent local equivs have the same target
If two local equivs are equivalent, so are their inverses.
Two equivalent local equivs have coinciding inverses on the target
Composition of local equivs respects equivalence
Restriction of local equivs respects equivalence
Composition of a local equiv and its inverse is equivalent to the restriction of the identity to the source
Composition of the inverse of a local equiv and this local equiv is equivalent to the restriction of the identity to the target
The product of two local equivs, as a local equiv on the product.
A bijection between two sets s : set α and t : set β provides a local equivalence
between α and β.
Equations
- set.bij_on.to_local_equiv f s t hf = {to_fun := f, inv_fun := function.inv_fun_on f s, source := s, target := t, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}
A map injective on a subset of its domain provides a local equivalence.
Equations
- set.inj_on.to_local_equiv f s hf = set.bij_on.to_local_equiv f s (f '' s) _