mathlib documentation

data.equiv.local_equiv

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:

Each of these implementations has pros and cons.

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.

A very basic tactic to show that sets showing up in manifolds coincide or are included in one another.

@[nolint]
structure local_equiv  :
Type u_5Type u_6Type (max u_5 u_6)

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.

def equiv.to_local_equiv {α : Type u_1} {β : Type u_2} :
α βlocal_equiv α β

Associating a local_equiv to an equiv

Equations
def local_equiv.symm {α : Type u_1} {β : Type u_2} :
local_equiv α βlocal_equiv β α

The inverse of a local equiv

Equations
@[instance]
def local_equiv.has_coe_to_fun {α : Type u_1} {β : Type u_2} :

Equations
@[simp]
theorem local_equiv.coe_mk {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) (s : set α) (t : set β) (ml : ∀ {x : α}, x sf x t) (mr : ∀ {x : β}, x tg x s) (il : ∀ {x : α}, x sg (f x) = x) (ir : ∀ {x : β}, x tf (g x) = x) :
{to_fun := f, inv_fun := g, source := s, target := t, map_source' := ml, map_target' := mr, left_inv' := il, right_inv' := ir} = f

@[simp]
theorem local_equiv.coe_symm_mk {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) (s : set α) (t : set β) (ml : ∀ {x : α}, x sf x t) (mr : ∀ {x : β}, x tg x s) (il : ∀ {x : α}, x sg (f x) = x) (ir : ∀ {x : β}, x tf (g x) = x) :
({to_fun := f, inv_fun := g, source := s, target := t, map_source' := ml, map_target' := mr, left_inv' := il, right_inv' := ir}.symm) = g

@[simp]
theorem local_equiv.to_fun_as_coe {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

@[simp]
theorem local_equiv.inv_fun_as_coe {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

@[simp]
theorem local_equiv.map_source {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {x : α} :
x e.sourcee x e.target

theorem local_equiv.maps_to {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

@[simp]
theorem local_equiv.map_target {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {x : β} :
x e.target(e.symm) x e.source

theorem local_equiv.symm_maps_to {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

@[simp]
theorem local_equiv.left_inv {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {x : α} :
x e.source(e.symm) (e x) = x

theorem local_equiv.left_inv_on {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

@[simp]
theorem local_equiv.right_inv {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {x : β} :
x e.targete ((e.symm) x) = x

theorem local_equiv.right_inv_on {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

def local_equiv.to_equiv {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

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

Equations
@[simp]
theorem local_equiv.symm_source {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

@[simp]
theorem local_equiv.symm_target {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

@[simp]
theorem local_equiv.symm_symm {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
e.symm.symm = e

theorem local_equiv.bij_on_source {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

A local equiv induces a bijection between its source and target

theorem local_equiv.image_eq_target_inter_inv_preimage {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {s : set α} :
s e.sourcee '' s = e.target (e.symm) ⁻¹' s

theorem local_equiv.image_inter_source_eq {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set α) :

theorem local_equiv.image_inter_source_eq' {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set α) :

theorem local_equiv.symm_image_eq_source_inter_preimage {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {s : set β} :
s e.target(e.symm) '' s = e.source e ⁻¹' s

theorem local_equiv.symm_image_inter_target_eq {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set β) :

theorem local_equiv.symm_image_inter_target_eq' {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set β) :

theorem local_equiv.source_inter_preimage_inv_preimage {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set α) :

theorem local_equiv.target_inter_inv_preimage_preimage {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set β) :

theorem local_equiv.image_source_eq_target {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

theorem local_equiv.source_subset_preimage_target {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

theorem local_equiv.inv_image_target_eq_source {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

theorem local_equiv.target_subset_preimage_source {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

@[ext]
theorem local_equiv.ext {α : Type u_1} {β : Type u_2} {e e' : local_equiv α β} :
(∀ (x : α), e x = e' x)(∀ (x : β), (e.symm) x = (e'.symm) x)e.source = e'.sourcee = e'

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

def local_equiv.restr {α : Type u_1} {β : Type u_2} :
local_equiv α βset αlocal_equiv α β

Restricting a local equivalence to e.source ∩ s

Equations
@[simp]
theorem local_equiv.restr_coe {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set α) :
(e.restr s) = e

@[simp]
theorem local_equiv.restr_coe_symm {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set α) :
((e.restr s).symm) = (e.symm)

@[simp]
theorem local_equiv.restr_source {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set α) :
(e.restr s).source = e.source s

@[simp]
theorem local_equiv.restr_target {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set α) :

theorem local_equiv.restr_eq_of_source_subset {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} :
e.source se.restr s = e

@[simp]
theorem local_equiv.restr_univ {α : Type u_1} {β : Type u_2} {e : local_equiv α β} :

def local_equiv.refl (α : Type u_1) :

The identity local equiv

Equations
@[simp]
theorem local_equiv.refl_source {α : Type u_1} :

@[simp]
theorem local_equiv.refl_target {α : Type u_1} :

@[simp]
theorem local_equiv.refl_coe {α : Type u_1} :

@[simp]
theorem local_equiv.refl_symm {α : Type u_1} :

@[simp]
theorem local_equiv.refl_restr_source {α : Type u_1} (s : set α) :

@[simp]
theorem local_equiv.refl_restr_target {α : Type u_1} (s : set α) :

def local_equiv.of_set {α : Type u_1} :
set αlocal_equiv α α

The identity local equiv on a set s

Equations
@[simp]
theorem local_equiv.of_set_source {α : Type u_1} (s : set α) :

@[simp]
theorem local_equiv.of_set_target {α : Type u_1} (s : set α) :

@[simp]
theorem local_equiv.of_set_coe {α : Type u_1} (s : set α) :

@[simp]
theorem local_equiv.of_set_symm {α : Type u_1} (s : set α) :

def local_equiv.trans' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : local_equiv α β) (e' : local_equiv β γ) :
e.target = e'.sourcelocal_equiv α γ

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

Equations
def local_equiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
local_equiv α βlocal_equiv β γlocal_equiv α γ

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

Equations
@[simp]
theorem local_equiv.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : local_equiv α β) (e' : local_equiv β γ) :
(e e') = e' e

@[simp]
theorem local_equiv.coe_trans_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : local_equiv α β) (e' : local_equiv β γ) :
((e e').symm) = (e.symm) (e'.symm)

theorem local_equiv.trans_symm_eq_symm_trans_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : local_equiv α β) (e' : local_equiv β γ) :
(e e').symm = e'.symm e.symm

@[simp]
theorem local_equiv.trans_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : local_equiv α β) (e' : local_equiv β γ) :

theorem local_equiv.trans_source' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : local_equiv α β) (e' : local_equiv β γ) :

theorem local_equiv.trans_source'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : local_equiv α β) (e' : local_equiv β γ) :
(e e').source = (e.symm) '' (e.target e'.source)

theorem local_equiv.image_trans_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : local_equiv α β) (e' : local_equiv β γ) :
e '' (e e').source = e.target e'.source

@[simp]
theorem local_equiv.trans_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : local_equiv α β) (e' : local_equiv β γ) :

theorem local_equiv.trans_target' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : local_equiv α β) (e' : local_equiv β γ) :

theorem local_equiv.trans_target'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : local_equiv α β) (e' : local_equiv β γ) :
(e e').target = e' '' (e'.source e.target)

theorem local_equiv.inv_image_trans_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : local_equiv α β) (e' : local_equiv β γ) :
(e'.symm) '' (e e').target = e'.source e.target

theorem local_equiv.trans_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : local_equiv α β) (e' : local_equiv β γ) (e'' : local_equiv γ δ) :
(e e') e'' = e e' e''

@[simp]
theorem local_equiv.trans_refl {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

@[simp]
theorem local_equiv.refl_trans {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

theorem local_equiv.trans_refl_restr {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set β) :

theorem local_equiv.trans_refl_restr' {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set β) :

theorem local_equiv.restr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : local_equiv α β) (e' : local_equiv β γ) (s : set α) :
e.restr s e' = (e e').restr s

def local_equiv.eq_on_source {α : Type u_1} {β : Type u_2} :
local_equiv α βlocal_equiv α β → Prop

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.

Equations
@[instance]
def local_equiv.eq_on_source_setoid {α : Type u_1} {β : Type u_2} :

eq_on_source is an equivalence relation

Equations
theorem local_equiv.eq_on_source_refl {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
e e

theorem local_equiv.eq_on_source.source_eq {α : Type u_1} {β : Type u_2} {e e' : local_equiv α β} :
e e'e.source = e'.source

Two equivalent local equivs have the same source

theorem local_equiv.eq_on_source.eq_on {α : Type u_1} {β : Type u_2} {e e' : local_equiv α β} :
e e'set.eq_on e e' e.source

Two equivalent local equivs coincide on the source

theorem local_equiv.eq_on_source.target_eq {α : Type u_1} {β : Type u_2} {e e' : local_equiv α β} :
e e'e.target = e'.target

Two equivalent local equivs have the same target

theorem local_equiv.eq_on_source.symm' {α : Type u_1} {β : Type u_2} {e e' : local_equiv α β} :
e e'e.symm e'.symm

If two local equivs are equivalent, so are their inverses.

theorem local_equiv.eq_on_source.symm_eq_on {α : Type u_1} {β : Type u_2} {e e' : local_equiv α β} :
e e'set.eq_on (e.symm) (e'.symm) e.target

Two equivalent local equivs have coinciding inverses on the target

theorem local_equiv.eq_on_source.trans' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {e e' : local_equiv α β} {f f' : local_equiv β γ} :
e e'f f'e f e' f'

Composition of local equivs respects equivalence

theorem local_equiv.eq_on_source.restr {α : Type u_1} {β : Type u_2} {e e' : local_equiv α β} (he : e e') (s : set α) :
e.restr s e'.restr s

Restriction of local equivs respects equivalence

theorem local_equiv.eq_on_source.source_inter_preimage_eq {α : Type u_1} {β : Type u_2} {e e' : local_equiv α β} (he : e e') (s : set β) :

Preimages are respected by equivalence

theorem local_equiv.trans_self_symm {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

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

theorem local_equiv.trans_symm_self {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :

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

theorem local_equiv.eq_of_eq_on_source_univ {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) :
e e'e.source = set.unive.target = set.unive = e'

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

def local_equiv.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} :
local_equiv α βlocal_equiv γ δlocal_equiv × γ) × δ)

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

Equations
@[simp]
theorem local_equiv.prod_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : local_equiv α β) (e' : local_equiv γ δ) :

@[simp]
theorem local_equiv.prod_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : local_equiv α β) (e' : local_equiv γ δ) :

@[simp]
theorem local_equiv.prod_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : local_equiv α β) (e' : local_equiv γ δ) :
(e.prod e') = λ (p : α × γ), (e p.fst, e' p.snd)

theorem local_equiv.prod_coe_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : local_equiv α β) (e' : local_equiv γ δ) :
((e.prod e').symm) = λ (p : β × δ), ((e.symm) p.fst, (e'.symm) p.snd)

@[simp]
theorem local_equiv.prod_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : local_equiv α β) (e' : local_equiv γ δ) :
(e.prod e').symm = e.symm.prod e'.symm

@[simp]
theorem local_equiv.prod_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {η : Type u_5} {ε : Type u_6} (e : local_equiv α β) (f : local_equiv β γ) (e' : local_equiv δ η) (f' : local_equiv η ε) :
e.prod e' f.prod f' = (e f).prod (e' f')

@[simp]
theorem set.bij_on.to_local_equiv_source {α : Type u_1} {β : Type u_2} [nonempty α] (f : α → β) (s : set α) (t : set β) (hf : set.bij_on f s t) :

@[simp]
theorem set.bij_on.to_local_equiv_to_fun {α : Type u_1} {β : Type u_2} [nonempty α] (f : α → β) (s : set α) (t : set β) (hf : set.bij_on f s t) (ᾰ : α) :
(set.bij_on.to_local_equiv f s t hf) = f ᾰ

@[simp]
theorem set.bij_on.to_local_equiv_target {α : Type u_1} {β : Type u_2} [nonempty α] (f : α → β) (s : set α) (t : set β) (hf : set.bij_on f s t) :

def set.bij_on.to_local_equiv {α : Type u_1} {β : Type u_2} [nonempty α] (f : α → β) (s : set α) (t : set β) :
set.bij_on f s tlocal_equiv α β

A bijection between two sets s : set α and t : set β provides a local equivalence between α and β.

Equations
@[simp]
theorem set.bij_on.to_local_equiv_inv_fun {α : Type u_1} {β : Type u_2} [nonempty α] (f : α → β) (s : set α) (t : set β) (hf : set.bij_on f s t) (b : β) :

@[simp]
def set.inj_on.to_local_equiv {α : Type u_1} {β : Type u_2} [nonempty α] (f : α → β) (s : set α) :
set.inj_on f slocal_equiv α β

A map injective on a subset of its domain provides a local equivalence.

Equations
@[simp]
theorem equiv.to_local_equiv_coe {α : Type u_1} {β : Type u_2} (e : α β) :

@[simp]
theorem equiv.to_local_equiv_symm_coe {α : Type u_1} {β : Type u_2} (e : α β) :

@[simp]
theorem equiv.to_local_equiv_source {α : Type u_1} {β : Type u_2} (e : α β) :

@[simp]
theorem equiv.to_local_equiv_target {α : Type u_1} {β : Type u_2} (e : α β) :

@[simp]

@[simp]
theorem equiv.symm_to_local_equiv {α : Type u_1} {β : Type u_2} (e : α β) :

@[simp]
theorem equiv.trans_to_local_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (e' : β γ) :