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 ∩ v
is 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_fun
andinv_fun
outside ofsource
andtarget
). 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_source
that captures this right notion of equality, and show that many properties are invariant under this equivalence relation.
Local coding conventions #
If a lemma deals with the intersection of a set with either source or target of a local_equiv
,
then it should use e.source ∩ s
or e.target ∩ t
, not s ∩ e.source
or t ∩ e.target
.
The simpset mfld_simps
records several simp lemmas that are
especially useful in manifolds. It is a subset of the whole set of simp lemmas, but it makes it
possible to have quicker proofs (when used with squeeze_simp
or simp only
) while retaining
readability.
The typical use case is the following, in a file on manifolds:
If simp [foo, bar]
is slow, replace it with squeeze_simp [foo, bar] with mfld_simps
and paste
its output. The list of lemmas should be reasonable (contrary to the output of
squeeze_simp [foo, bar]
which might contain tens of lemmas), and the outcome should be quick
enough.
Common @[simps]
configuration options used for manifold-related declarations.
Equations
- mfld_cfg = {attrs := [name.mk_string "simp" name.anonymous, name.mk_string "mfld_simps" name.anonymous], short_name := ff, simp_rhs := ff, type_md := tactic.transparency.instances, rhs_md := tactic.transparency.none, fully_applied := ff, not_recursive := [name.mk_string "prod" name.anonymous, name.mk_string "pprod" name.anonymous], trace := ff}
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, inv_fun := ⇑(e.symm), 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 β}
See Note [custom simps projection]
Equations
Create a copy of a local_equiv
providing better definitional equalities.
Equations
- e.copy f hf g hg s hs t ht = {to_fun := f, inv_fun := g, source := s, target := t, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}
Associating to a local_equiv an equiv between the source and the target
We say that t : set β
is an image of s : set α
under a local equivalence if
any of the following equivalent conditions hold:
e '' (e.source ∩ s) = e.target ∩ t
;e.source ∩ e ⁻¹ t = e.source ∩ s
;∀ x ∈ e.source, e x ∈ t ↔ x ∈ s
(this one is used in the definition).
Restrict a local_equiv
to a pair of corresponding sets.
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.
Combine two local_equiv
s using set.piecewise
. The source of the new local_equiv
is
s.ite e.source e'.source = e.source ∩ s ∪ e'.source \ s
, and similarly for target. The function
sends e.source ∩ s
to e.target ∩ t
using e
and e'.source \ s
to e'.target \ t
using e'
,
and similarly for the inverse function. The definition assumes e.is_image s t
and
e'.is_image s t
.
Combine two local_equiv
s with disjoint sources and disjoint targets. We reuse
local_equiv.piecewise
, then override source
and target
to ensure better definitional
equalities.
The product of a family of local equivs, as a local equiv on the pi type.
Equations
- local_equiv.pi ei = {to_fun := λ (f : Π (i : ι), αi i) (i : ι), ⇑(ei i) (f i), inv_fun := λ (f : Π (i : ι), βi i) (i : ι), ⇑((ei i).symm) (f i), source := set.univ.pi (λ (i : ι), (ei i).source), target := set.univ.pi (λ (i : ι), (ei i).target), map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}
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) _