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.

Contrary to equivs, we do not register the coercion to functions and we use explicitly to_fun and inv_fun: coercions create numerous unification problems for manifolds.

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 α and option β, 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 ∩ v is not the "same" as v ∩ 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_fun and inv_fun outside of source and target). 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 relation eq_on_source that captures this right notion of equality, and show that many properties are invariant under this equivalence relation.

local_equiv

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.

equiv.to_local_equiv

Associating a local_equiv to an equiv

local_equiv.to_equiv

Associating to a local_equiv an equiv between the source and the target

local_equiv.symm

The inverse of a local equiv

local_equiv.bij_on_source

A local equiv induces a bijection between its source and target

local_equiv.ext

Two local equivs that have the same source, same to_fun and same inv_fun, coincide.

local_equiv.restr

Restricting a local equivalence to e.source ∩ s

local_equiv.refl

The identity local equiv

local_equiv.of_set

The identity local equiv on a set s

local_equiv.trans'

Composing two local equivs if the target of the first coincides with the source of the second.

local_equiv.trans

Composing two local equivs, by restricting to the maximal domain where their composition is well defined.

local_equiv.eq_on_source

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.

local_equiv.eq_on_source_setoid

eq_on_source is an equivalence relation

local_equiv.eq_on_source_symm

If two local equivs are equivalent, so are their inverses

local_equiv.source_eq_of_eq_on_source

Two equivalent local equivs have the same source

local_equiv.target_eq_of_eq_on_source

Two equivalent local equivs have the same target

local_equiv.apply_eq_of_eq_on_source

Two equivalent local equivs coincide on the source

local_equiv.inv_apply_eq_of_eq_on_source

Two equivalent local equivs have coinciding inverses on the target

local_equiv.eq_on_source_trans

Composition of local equivs respects equivalence

local_equiv.eq_on_source_restr

Restriction of local equivs respects equivalence

local_equiv.eq_on_source_preimage

Preimages are respected by equivalence

local_equiv.trans_self_symm

Composition of a local equiv and its inverse is equivalent to the restriction of the identity to the source

local_equiv.trans_symm_self

Composition of the inverse of a local equiv and this local equiv is equivalent to the restriction of the identity to the target

local_equiv.eq_of_eq_on_source_univ

Two equivalent local equivs are equal when the source and target are univ

local_equiv.prod

The product of two local equivs, as a local equiv on the product.