basic.lean

/-
Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel

Manifolds based on any structure groupoid of homeomorphisms.

long term TODO:
*  ≤ on groupoids, interfaced with type classes, to say that a C^k manifold is automatically
a C^1 manifold when 1 ≤ k
*  definition of C^k regularity classes, and C^k manifolds
*  tangent bundle of a C^k manifold, as a C^{k-1} manifold
*  any C^1 manifold admits a C^∞ structure (would require some integration to define convolution)
*  any two C^∞ structures on a C^1 manifold are diffeomorphic
*  Whitney (weak version): any C^k real manifold embeds in ℝ^N for large enough N
*  submanifolds, embeddings, and so on
-/


import topology.opens tactic.tidy

section continuous
variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
variables [topological_space α] [topological_space β] [topological_space γ]

open set filter

/-- A function between topological spaces is continuous iff it is continuous on the
whole space. -/
def continuous_iff_continuous_on_univ {f : α → β} : continuous f ↔ continuous_on f univ :=
by simp [continuous_iff_continuous_at, continuous_on, continuous_at, continuous_at_within,
         nhds_within_univ]

lemma continuous_on.comp {f : α → β} {g : β → γ} {s : set α} {t : set β}
  (hf : continuous_on f s) (hg : continuous_on g t) (h : f '' s ⊆ t) :
  continuous_on (g ∘ f) s :=
begin
  assume x hx,
  have : tendsto f (principal s) (principal t),
    by { rw tendsto_principal_principal, exact λx hx, h (mem_image_of_mem _ hx) },
  have : tendsto f (nhds_within x s) (principal t) :=
    tendsto_le_left lattice.inf_le_right this,
  have : tendsto f (nhds_within x s) (nhds_within (f x) t) :=
    tendsto_inf.2 ⟨hf x hx, this⟩,
  exact tendsto.comp this (hg _ (h (mem_image_of_mem _ hx)))
end

lemma continuous_on.restr {f : α → β} {s t : set α} (hf : continuous_on f s) (h : t ⊆ s)  :
  continuous_on f t :=
λx hx, tendsto_le_left (nhds_within_mono _ h) (hf x (h hx))

lemma continuous_on.preimage_open_of_open {f : α → β} {s : set α} {t : set β}
  (hf : continuous_on f s) (hs : is_open s) (ht : is_open t) : is_open (s ∩ f⁻¹' t) :=
begin
  rcases continuous_on_iff'.1 hf t ht with ⟨u, hu⟩,
  rw [inter_comm, hu.2],
  apply is_open_inter hu.1 hs
end

lemma continuous_on.preimage_interior_subset_interior_preimage {f : α → β} {s : set α} {t : set β}
  (hf : continuous_on f s) (hs : is_open s) : s ∩ f⁻¹' (interior t) ⊆ s ∩ interior (f⁻¹' t) :=
calc s ∩ f ⁻¹' (interior t)
     = interior (s ∩ f ⁻¹' (interior t)) :
       (interior_eq_of_open (hf.preimage_open_of_open hs is_open_interior)).symm
    ... ⊆ interior (s ∩ f ⁻¹' t) :
        interior_mono (inter_subset_inter (subset.refl _) (preimage_mono interior_subset))
    ... = s ∩ interior (f ⁻¹' t) :
      by rw [interior_inter, interior_eq_of_open hs]

end continuous


open function set

variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}

structure local_equiv (α : Type*) (β : Type*) :=
(to_fun  : α → β)
(inv_fun : β → α)
(source  : set α)
(target  : set β)
(to_map  : ∀x ∈ source, to_fun x ∈ target)
(inv_map : ∀x ∈ target, inv_fun x ∈ source)
(to_inv  : ∀x ∈ source, inv_fun (to_fun x) = x)
(inv_to  : ∀x ∈ target, to_fun (inv_fun x) = x)

def equiv.to_local_equiv (e : equiv α β) : local_equiv α β :=
{ to_fun := e.to_fun,
  inv_fun := e.inv_fun,
  source  := univ,
  target  := univ,
  to_map  := λx hx, mem_univ _,
  inv_map := λy hy, mem_univ _,
  to_inv  := λx hx, e.left_inv x,
  inv_to  := λx hx, e.right_inv x }

namespace local_equiv

instance : has_coe_to_fun (local_equiv α β) :=
⟨_, to_fun⟩

protected def to_equiv (e : local_equiv α β) : equiv (e.source) (e.target) :=
{ to_fun    := λ⟨x, hx⟩, ⟨e.to_fun x, e.to_map x hx⟩,
  inv_fun   := λ⟨y, hy⟩, ⟨e.inv_fun y, e.inv_map y hy⟩,
  left_inv  := λ⟨x, hx⟩, subtype.eq $ e.to_inv _ hx,
  right_inv := λ⟨y, hy⟩, subtype.eq $ e.inv_to _ hy }

protected def symm (e : local_equiv α β) : local_equiv β α :=
{ to_fun := e.inv_fun,
  inv_fun := e.to_fun,
  source  := e.target,
  target  := e.source,
  to_map  := e.inv_map,
  inv_map := e.to_map,
  to_inv  := e.inv_to,
  inv_to  := e.to_inv }

@[simp] lemma symm_to_fun (e : local_equiv α β) : e.symm.to_fun = e.inv_fun := rfl
@[simp] lemma symm_inv_fun (e : local_equiv α β) : e.symm.inv_fun = e.to_fun := rfl
@[simp] lemma symm_source (e : local_equiv α β) : e.symm.source = e.target := rfl
@[simp] lemma symm_target (e : local_equiv α β) : e.symm.target = e.source := rfl

@[simp] lemma symm_symm (e : local_equiv α β) : e.symm.symm = e := by cases e; refl

protected def refl (α : Type*) : local_equiv α α := (equiv.refl α).to_local_equiv

@[simp] lemma refl_source : (local_equiv.refl α).source = univ := rfl
@[simp] lemma refl_target : (local_equiv.refl α).target = univ := rfl
@[simp] lemma refl_to_fun : (local_equiv.refl α).to_fun = id := rfl
@[simp] lemma refl_inv_fun : (local_equiv.refl α).inv_fun = id := rfl

lemma bij_on_to_fun (e : local_equiv α β) :
  bij_on e.to_fun e.source e.target :=
bij_on_of_inv_on e.to_map e.inv_map ⟨e.to_inv, e.inv_to⟩

lemma to_fun_image_eq_target_inter_inv_fun_preimage (e : local_equiv α β) {s : set α} (h : s ⊆ e.source) :
  e.to_fun '' s = e.target ∩ e.inv_fun⁻¹' s :=
begin
  refine subset.antisymm (λx hx, _) (λx hx, _),
  { rcases (mem_image _ _ _).1 hx with ⟨y, ys, hy⟩,
    rw ← hy,
    split,
    { apply e.to_map,
      exact h ys },
    { rwa [mem_preimage_eq, e.to_inv],
      exact h ys } },
  { have : x = e.to_fun (e.inv_fun x),
    { rw e.inv_to,
      exact hx.1 },
    rw this,
    exact mem_image_of_mem _ hx.2 }
end

lemma inv_fun_image_eq_source_inter_to_fun_preimage (e : local_equiv α β) {s : set β} (h : s ⊆ e.target) :
  e.inv_fun '' s = e.source ∩ e.to_fun⁻¹' s :=
e.symm.to_fun_image_eq_target_inter_inv_fun_preimage h

lemma source_inter_to_fun_inv_fun_preimage (e : local_equiv α β) {s : set α} :
  e.source ∩ e.to_fun⁻¹' (e.inv_fun ⁻¹' s) = e.source ∩ s :=
begin
  ext, split,
  { rintros ⟨hx, xs⟩,
    simp only [mem_preimage_eq] at xs,
    rw e.to_inv _ hx at xs,
    exact ⟨hx, xs⟩ },
  { rintros ⟨hx, xs⟩,
    simpa only [hx, true_and, mem_preimage_eq, mem_inter_eq, e.to_inv _ hx] }
end

lemma target_inter_inv_fun_to_fun_preimage (e : local_equiv α β) {s : set β} :
  e.target ∩ e.inv_fun⁻¹' (e.to_fun ⁻¹' s) = e.target ∩ s :=
e.symm.source_inter_to_fun_inv_fun_preimage

lemma bij_on_inv_fun (e : local_equiv α β) :
  bij_on e.inv_fun e.target e.source :=
e.symm.bij_on_to_fun

lemma image_source_eq_target (e : local_equiv α β) : e.to_fun '' e.source = e.target :=
image_eq_of_bij_on e.bij_on_to_fun

lemma source_subset_preimage_target (e : local_equiv α β) : e.source ⊆ e.to_fun ⁻¹' e.target :=
λx hx, e.to_map x hx

lemma image_target_eq_source (e : local_equiv α β) : e.inv_fun '' e.target = e.source :=
image_eq_of_bij_on e.bij_on_inv_fun

lemma target_subset_preimage_source (e : local_equiv α β) : e.target ⊆ e.inv_fun ⁻¹' e.source :=
λx hx, e.inv_map x hx

protected lemma eq (e : local_equiv α β) (e' : local_equiv α β)
(hto : e.to_fun = e'.to_fun) (hinv : e.inv_fun = e'.inv_fun) (hs : e.source = e'.source) : e = e' :=
begin
  have I := e.image_source_eq_target,
  have I' := e'.image_source_eq_target,
  cases e; cases e',
  simp at hto hinv hs I I',
  simp [hto, hinv, hs],
  rw [← I, ← I', hto, hs]
end

/-- Restricting a local equivalence to s ∩ e.source -/
protected def restr (e : local_equiv α β) (s : set α) : local_equiv α β :=
{ to_fun  := e.to_fun,
  inv_fun := e.inv_fun,
  source  := e.source ∩ s,
  target  := e.target ∩ e.inv_fun⁻¹' s,
  to_map  := λx hx, begin
    apply mem_inter,
    { apply e.to_map,
      exact hx.1 },
    { rw [mem_preimage_eq, e.to_inv],
      exact hx.2,
      exact hx.1 },
  end,
  inv_map := λy hy, begin
    apply mem_inter,
    { apply e.inv_map,
      exact hy.1 },
    { exact hy.2 },
  end,
  to_inv := λx hx, e.to_inv x hx.1,
  inv_to := λy hy, e.inv_to y hy.1 }

@[simp] lemma restr_to_fun (e : local_equiv α β) (s : set α) : (e.restr s).to_fun = e.to_fun := rfl
@[simp] lemma restr_inv_fun (e : local_equiv α β) (s : set α) : (e.restr s).inv_fun = e.inv_fun := rfl
@[simp] lemma restr_source (e : local_equiv α β) (s : set α) : (e.restr s).source = e.source ∩ s := rfl
@[simp] lemma restr_target (e : local_equiv α β) (s : set α) :
  (e.restr s).target = e.target ∩ e.inv_fun⁻¹' s := rfl


@[simp] lemma refl_restr_source (s : set α) : ((local_equiv.refl α).restr s).source = s :=
by simp

@[simp] lemma refl_restr_target (s : set α) : ((local_equiv.refl α).restr s).target = s :=
begin
  change univ ∩ id⁻¹' s = s,
  simp [preimage_id]
end

/-- Composing two local equivs if the target of the source coincides with the source of the
second. -/
protected def trans' (e : local_equiv α β) (e' : local_equiv β γ) (h : e.target = e'.source) :
  local_equiv α γ :=
{ to_fun := e'.to_fun ∘ e.to_fun,
  inv_fun := e.inv_fun ∘ e'.inv_fun,
  source := e.source,
  target := e'.target,
  to_map := λx hx, begin
    apply e'.to_map,
    rw ← h,
    apply e.to_map x hx
  end,
  inv_map := λy hy, begin
     apply e.inv_map,
     rw h,
     apply e'.inv_map y hy
  end,
  to_inv := λx hx, begin
    change e.inv_fun (e'.inv_fun (e'.to_fun (e.to_fun x))) = x,
    rw e'.to_inv,
    { exact e.to_inv x hx },
    { rw ← h, exact e.to_map x hx }
  end,
  inv_to := λy hy, begin
    change e'.to_fun (e.to_fun (e.inv_fun (e'.inv_fun y))) = y,
    rw e.inv_to,
    { exact e'.inv_to y hy },
    { rw h, exact e'.inv_map y hy }
  end }

/-- Composing two local equivs, by restricting to the maximal domain where their composition
is well defined. -/
protected def trans (e : local_equiv α β) (e' : local_equiv β γ) : local_equiv α γ :=
  local_equiv.trans' (e.symm.restr (e'.source)).symm (e'.restr (e.target)) (inter_comm _ _)

lemma trans_source (e : local_equiv α β) (e' : local_equiv β γ) :
  (e.trans e').source = e.source ∩ e.to_fun ⁻¹' e'.source := rfl

lemma trans_source' (e : local_equiv α β) (e' : local_equiv β γ) :
  (e.trans e').source = e.source ∩ e.to_fun ⁻¹' (e.target ∩ e'.source) :=
begin
  have A := calc
    e.source ∩ e.to_fun ⁻¹' (e.target ∩ e'.source) =
    (e.source ∩ e.to_fun ⁻¹' (e.target)) ∩ e.to_fun ⁻¹' (e'.source) :
      by rw [preimage_inter, inter_assoc]
    ... = e.source ∩ e.to_fun ⁻¹' (e'.source) :
      by { congr' 1, apply inter_eq_self_of_subset_left e.source_subset_preimage_target }
    ... = (e.trans e').source : rfl,
  exact A.symm
end

lemma trans_source'' (e : local_equiv α β) (e' : local_equiv β γ) :
  (e.trans e').source = e.inv_fun '' (e.target ∩ e'.source) :=
begin
  rw [e.trans_source', e.inv_fun_image_eq_source_inter_to_fun_preimage, inter_comm],
  exact inter_subset_left _ _,
end

@[simp]lemma trans_to_fun (e : local_equiv α β) (e' : local_equiv β γ) :
  (e.trans e').to_fun = e'.to_fun ∘ e.to_fun := rfl

lemma trans_symm_eq_symm_trans_symm (e : local_equiv α β) (e' : local_equiv β γ) :
  (e.trans e').symm = e'.symm.trans e.symm :=
by cases e; cases e'; refl

lemma trans_assoc (e : local_equiv α β) (e' : local_equiv β γ) (e'' : local_equiv γ δ) :
  (e.trans e').trans e'' = e.trans (e'.trans e'') :=
begin
  apply local_equiv.eq,
  { refl },
  { refl },
  { change (e.source ∩ e.to_fun ⁻¹' e'.source) ∩ ((e.trans e').to_fun ⁻¹' e''.source)
      = e.source ∩ e.to_fun ⁻¹' (e'.source ∩ e'.to_fun ⁻¹' e''.source),
    rw [trans_to_fun, preimage_inter, @preimage_comp α β γ, inter_assoc] }
end

@[simp] lemma trans_refl (e : local_equiv α β) : e.trans (local_equiv.refl β) = e :=
begin
  apply local_equiv.eq,
  { refl },
  { refl },
  { rw trans_source,
    simp }
end

@[simp] lemma refl_trans (e : local_equiv α β) : (local_equiv.refl α).trans e = e :=
begin
  apply local_equiv.eq,
  { refl },
  { refl },
  { rw trans_source,
    simp [preimage_id] }
end

lemma trans_refl_restr (e : local_equiv α β) (s : set β) :
  e.trans ((local_equiv.refl β).restr s) = e.restr (e.to_fun ⁻¹' s) :=
begin
  apply local_equiv.eq,
  { refl },
  { refl },
  { rw trans_source, simp }
end

lemma trans_refl_restr' (e : local_equiv α β) (s : set β) :
  e.trans ((local_equiv.refl β).restr s) = e.restr (e.source ∩ e.to_fun ⁻¹' s) :=
begin
  apply local_equiv.eq,
  { refl },
  { refl },
  { rw trans_source, simp, rw [← inter_assoc, inter_self] }
end

lemma restr_trans (e : local_equiv α β) (e' : local_equiv β γ) (s : set α) :
  (e.restr s).trans e' = (e.trans e').restr s :=
begin
  apply local_equiv.eq,
  { refl },
  { refl },
  { simp [trans_source, inter_comm], rwa inter_assoc }
end

lemma equiv_to_local_equiv_trans (e : equiv α β) (e' : equiv β γ) :
  (e.trans e').to_local_equiv = e.to_local_equiv.trans e'.to_local_equiv :=
begin
  apply local_equiv.eq,
  { refl },
  { refl },
  { simp [trans_source, equiv.to_local_equiv] }
end

/-- `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. -/
def eq_on_source (e e' : local_equiv α β) : Prop :=
  e.source = e'.source ∧ (∀x ∈ e.source, e.to_fun x = e'.to_fun x)

/-- `eq_on_source` is an equivalence relation -/
instance eq_on_source_setoid : setoid (local_equiv α β) :=
{ r     := eq_on_source,
  iseqv := ⟨
    λe, by simp [eq_on_source],
    λe e' h, by { simp [eq_on_source, h.1.symm], exact λx hx, (h.2 x hx).symm },
    λe e' e'' h h', ⟨by rwa [← h'.1, ← h.1], λx hx, by { rw [← h'.2 x, h.2 x hx], rwa ← h.1 }⟩⟩ }

lemma eq_on_source_refl (e : local_equiv α β) : e ≈ e := setoid.refl _

/-- If two local equivs are equivalent, so are their inverses -/
lemma eq_on_source_symm (e e' : local_equiv α β) (h : e ≈ e') : e.symm ≈ e'.symm :=
begin
  have T : e.target = e'.target,
  { have : bij_on e'.to_fun e.source e.target := bij_on_of_eq_on h.2 e.bij_on_to_fun,
    have A : e'.to_fun '' e.source = e.target := image_eq_of_bij_on this,
    rw [h.1, image_eq_of_bij_on e'.bij_on_to_fun] at A,
    exact A.symm },
  refine ⟨T, λx hx, _⟩,
  change e.inv_fun x = e'.inv_fun x,
  have xt : x ∈ e.target := hx,
  rw T at xt,
  have e's : e'.inv_fun x ∈ e.source, by { rw h.1, apply e'.inv_map _ xt },
  have A : e.to_fun (e.inv_fun x) = x := e.inv_to _ hx,
  have B : e.to_fun (e'.inv_fun x) = x,
    by { rw h.2, exact e'.inv_to _ xt, exact e's },
  apply inj_on_of_bij_on e.bij_on_to_fun (e.inv_map _ hx) e's,
  rw [A, B]
end

/-- Two equivalent local equivs have the same source -/
lemma source_eq_of_eq_on_source (e e' : local_equiv α β) (h : e ≈ e') : e.source = e'.source :=
h.1

/-- Two equivalent local equivs have the same target -/
lemma target_eq_of_eq_on_source (e e' : local_equiv α β) (h : e ≈ e') : e.target = e'.target :=
(eq_on_source_symm e e' h).1

/-- Two equivalent local equivs have coinciding `to_fun` on the source -/
lemma to_fun_eq_of_eq_on_source (e e' : local_equiv α β) (h : e ≈ e') {x : α} (hx : x ∈ e.source) :
  e.to_fun x = e'.to_fun x :=
h.2 x hx

/-- Two equivalent local equivs have coinciding `inv_fun` on the target -/
lemma inv_fun_eq_of_eq_on_source (e e' : local_equiv α β) (h : e ≈ e') {x : β} (hx : x ∈ e.target) :
  e.inv_fun x = e'.inv_fun x :=
(eq_on_source_symm e e' h).2 x hx

/-- Composition of local equivs respects equivalence -/
lemma eq_on_source_trans (e e' : local_equiv α β) (f f' : local_equiv β γ)
  (he : e ≈ e') (hf : f ≈ f') : e.trans f ≈ e'.trans f' :=
begin
  split,
  { have : e.target = e'.target := (eq_on_source_symm e e' he).1,
    rw [trans_source'', trans_source'', ← this, ← hf.1],
    exact image_eq_image_of_eq_on (λx hx, (eq_on_source_symm e e' he).2 x hx.1) },
  { assume x hx,
    rw trans_source at hx,
    have : e.to_fun x = e'.to_fun x := he.2 x hx.1,
    rw [trans_to_fun, trans_to_fun, function.comp_apply, function.comp_apply, ← this],
    exact hf.2 _ hx.2 }
end

/-- Restriction of local equivs respects equivalence -/
lemma eq_on_source_restr (e e' : local_equiv α β) (he : e ≈ e') (s : set α) :
  e.restr s ≈ e'.restr s :=
begin
  split,
  { simp [he.1] },
  { assume x hx,
    simp at hx,
    exact he.2 x hx.1 }
end

/-- Composition of a local equiv and its inverse is equivalent to the restriction of the identity
to the source -/
lemma trans_self_symm (e : local_equiv α β) :
  e.trans e.symm ≈ (local_equiv.refl α).restr e.source :=
begin
  have A : (e.trans e.symm).source = e.source,
  { rw trans_source,
    unfold local_equiv.symm,
    simp [inter_eq_self_of_subset_left (source_subset_preimage_target _)] },
  refine ⟨by simp [A], λx hx, _⟩,
  rw A at hx,
  simp only [restr_to_fun, id.def, refl_to_fun],
  exact e.to_inv x hx
end

lemma trans_symm_self (e : local_equiv α β) :
  e.symm.trans e ≈ (local_equiv.refl β).restr e.target :=
trans_self_symm (e.symm)


end local_equiv











/-- local homeomorphisms, defined on open subsets of the space -/
structure local_homeomorph (α : Type*) (β : Type*) [topological_space α] [topological_space β]
  extends local_equiv α β :=
(open_source    : is_open source)
(open_target    : is_open target)
(continuous_to  : continuous_on to_fun source)
(continuous_inv : continuous_on inv_fun target)

/-- A homeomorphism induces a local homeomorphism on the whole space -/
def homeomorph.to_local_homeomorph [topological_space α] [topological_space β] (e : homeomorph α β) :
  local_homeomorph α β :=
{ open_source    := is_open_univ,
  open_target    := is_open_univ,
  continuous_to  := by { erw ← continuous_iff_continuous_on_univ, exact e.continuous_to_fun },
  continuous_inv := by { erw ← continuous_iff_continuous_on_univ, exact e.continuous_inv_fun },
  ..e.to_equiv.to_local_equiv }

section
variables [topological_space α] [topological_space β] (e : homeomorph α β)

@[simp] lemma homeomorph.to_local_homeomorph_source  : e.to_local_homeomorph.source = univ := rfl
@[simp] lemma homeomorph.to_local_homeomorph_target : e.to_local_homeomorph.target = univ := rfl
@[simp] lemma homeomorph.to_local_homeomorph_to_fun : e.to_local_homeomorph.to_fun = e.to_fun := rfl
@[simp] lemma homeomorph.to_local_homeomorph_inv_fun : e.to_local_homeomorph.inv_fun = e.inv_fun := rfl
end

namespace local_homeomorph

variables [topological_space α] [topological_space β] [topological_space γ] [topological_space δ]

lemma eq_of_local_equiv_eq {e : local_homeomorph α β} {e' : local_homeomorph α β}
  (h : e.to_local_equiv = e'.to_local_equiv) : e = e' :=
by {cases e, cases e', simpa }

/-- Preimage of interior or interior of preimage coincide for local homeomorphisms, when restricted
to the source. -/
lemma preimage_interior (e : local_homeomorph α β) (s : set β) :
  e.source ∩ e.to_fun ⁻¹' (interior s) = e.source ∩ interior (e.to_fun ⁻¹' s) :=
begin
  apply subset.antisymm,
  { exact e.continuous_to.preimage_interior_subset_interior_preimage e.open_source },
  { calc e.source ∩ interior (e.to_fun ⁻¹' s)
    = (e.source ∩ e.to_fun ⁻¹' e.target) ∩ interior (e.to_fun ⁻¹' s) : begin
        congr,
        apply (inter_eq_self_of_subset_left _).symm,
        apply local_equiv.source_subset_preimage_target,
      end
    ... = (e.source ∩ interior (e.to_fun ⁻¹' s)) ∩ (e.to_fun ⁻¹' e.target) :
      by simp [inter_comm, inter_assoc]
    ... = (e.source ∩ e.to_fun⁻¹' (e.inv_fun ⁻¹' (interior (e.to_fun ⁻¹' s)))) ∩ (e.to_fun ⁻¹' e.target) :
      by rw local_equiv.source_inter_to_fun_inv_fun_preimage
    ... = e.source ∩ e.to_fun⁻¹' (e.target ∩ e.inv_fun ⁻¹' (interior (e.to_fun⁻¹' s))) :
       by rw [inter_comm e.target, preimage_inter, inter_assoc]
    ... ⊆ e.source ∩ e.to_fun ⁻¹' (e.target ∩ interior (e.inv_fun ⁻¹' (e.to_fun⁻¹' s))) : begin
        apply inter_subset_inter (subset.refl _) (preimage_mono _),
        exact e.continuous_inv.preimage_interior_subset_interior_preimage e.open_target
      end
    ... = e.source ∩ e.to_fun ⁻¹' (interior (e.target ∩ e.inv_fun ⁻¹' (e.to_fun⁻¹' s))) :
      by rw [interior_inter, interior_eq_of_open e.open_target]
    ... = e.source ∩ e.to_fun ⁻¹' (interior (e.target ∩ s)) :
      by rw local_equiv.target_inter_inv_fun_to_fun_preimage
    ... = e.source ∩ e.to_fun ⁻¹' e.target ∩ e.to_fun ⁻¹' (interior s) :
      by rw [interior_inter, preimage_inter, interior_eq_of_open e.open_target, inter_assoc]
    ... = e.source ∩ e.to_fun ⁻¹' (interior s) : begin
        congr,
        apply inter_eq_self_of_subset_left,
        apply local_equiv.source_subset_preimage_target,
      end }
end

protected lemma eq (e : local_homeomorph α β) (e' : local_homeomorph α β)
(hto : e.to_fun = e'.to_fun) (hinv : e.inv_fun = e'.inv_fun) (hs : e.source = e'.source) : e = e' :=
eq_of_local_equiv_eq (local_equiv.eq e.to_local_equiv e'.to_local_equiv hto hinv hs)

/-- The inverse of a local homeomorphism -/
protected def symm (e : local_homeomorph α β) : local_homeomorph β α :=
{ open_source    := e.open_target,
  open_target    := e.open_source,
  continuous_to  := e.continuous_inv,
  continuous_inv := e.continuous_to,
  ..e.to_local_equiv.symm }

@[simp] lemma symm_to_fun (e : local_homeomorph α β) : e.symm.to_fun = e.inv_fun := rfl
@[simp] lemma symm_inv_fun (e : local_homeomorph α β) : e.symm.inv_fun = e.to_fun := rfl
@[simp] lemma symm_source (e : local_homeomorph α β) : e.symm.source = e.target := rfl
@[simp] lemma symm_target (e : local_homeomorph α β) : e.symm.target = e.source := rfl

@[simp] lemma symm_symm (e : local_homeomorph α β) : e.symm.symm = e :=
by cases e; cases e__to_local_equiv; refl

/-- The identity on the whole space as a local homeomorphism. -/
protected def refl (α : Type*) [topological_space α] : local_homeomorph α α :=
(homeomorph.refl α).to_local_homeomorph

@[simp] lemma refl_source : (local_homeomorph.refl α).source = univ := rfl
@[simp] lemma refl_target : (local_homeomorph.refl α).target = univ := rfl
@[simp] lemma refl_to_fun : (local_homeomorph.refl α).to_fun = id := rfl
@[simp] lemma refl_inv_fun : (local_homeomorph.refl α).inv_fun = id := rfl

/-- Composition of two local homeomorphisms when the target of the first and the source of
the second coincide. -/
protected def trans' (e : local_homeomorph α β) (e' : local_homeomorph β γ)
  (h : e.target = e'.source) : local_homeomorph α γ :=
{ open_source := e.open_source,
  open_target := e'.open_target,
  continuous_to := begin
    apply continuous_on.comp e.continuous_to e'.continuous_to,
    rw [e.to_local_equiv.image_source_eq_target, h]
  end,
  continuous_inv := begin
    apply continuous_on.comp e'.continuous_inv e.continuous_inv,
    rw [e'.to_local_equiv.image_target_eq_source, h],
  end,
  ..local_equiv.trans' e.to_local_equiv e'.to_local_equiv h }

/-- 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 -/
protected def restr (e : local_homeomorph α β) (s : set α) : local_homeomorph α β :=
{ open_source := is_open_inter e.open_source is_open_interior,
  open_target := begin
    simp only [local_equiv.restr],
    have : e.inv_fun ⁻¹' e.source ∩ e.target = e.target :=
      inter_eq_self_of_subset_right e.to_local_equiv.target_subset_preimage_source,
    rcases continuous_on_iff'.1 e.continuous_inv (e.source ∩ interior s)
      (is_open_inter e.open_source is_open_interior) with ⟨u, hu⟩,
    rw [preimage_inter, inter_assoc, inter_comm _ e.target, ← inter_assoc, this] at hu,
    rw hu.2,
    exact is_open_inter hu.1 e.open_target
  end,
  continuous_to  := e.continuous_to.restr (inter_subset_left _ _),
  continuous_inv := e.continuous_inv.restr (inter_subset_left _ _),
  ..e.to_local_equiv.restr (interior s) }

@[simp] lemma restr_source (e : local_homeomorph α β) (s : set α) :
  (e.restr s).source = e.source ∩ interior s := rfl

lemma restr_source' (e : local_homeomorph α β) (s : set α) (hs : is_open s) :
  (e.restr s).source = e.source ∩ s :=
by rw [e.restr_source, interior_eq_of_open hs]

lemma restr_to_local_equiv (e : local_homeomorph α β) (s : set α) :
  (e.restr s).to_local_equiv = e.to_local_equiv.restr (interior s) := rfl

lemma restr_to_local_equiv' (e : local_homeomorph α β) (s : set α) (hs : is_open s):
  (e.restr s).to_local_equiv = e.to_local_equiv.restr s :=
by rw [e.restr_to_local_equiv, interior_eq_of_open hs]

/-- Restricting a local homeomorphism `e` to `e.source ∩ s` when `s` is open. This is less easy
to use than restr 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 -/
protected def restr_open (e : local_homeomorph α β) (s : set α) (hs : is_open s) :
  local_homeomorph α β :=
{ open_source := is_open_inter e.open_source hs,
  open_target := begin
        simp only [local_equiv.restr],
    have : e.inv_fun ⁻¹' e.source ∩ e.target = e.target :=
      inter_eq_self_of_subset_right e.to_local_equiv.target_subset_preimage_source,
    rcases continuous_on_iff'.1 e.continuous_inv (e.source ∩ s)
      (is_open_inter e.open_source hs) with ⟨u, hu⟩,
    rw [preimage_inter, inter_assoc, inter_comm _ e.target, ← inter_assoc, this] at hu,
    rw hu.2,
    exact is_open_inter hu.1 e.open_target
  end,
  continuous_to  := e.continuous_to.restr (inter_subset_left _ _),
  continuous_inv := e.continuous_inv.restr (inter_subset_left _ _),
  ..e.to_local_equiv.restr s}

@[simp] lemma restr_open_source (e : local_homeomorph α β) (s : set α) (hs : is_open s):
  (e.restr_open s hs).source = e.source ∩ s := rfl

lemma restr_open_to_local_equiv (e : local_homeomorph α β) (s : set α) (hs : is_open s) :
  (e.restr_open s hs).to_local_equiv = e.to_local_equiv.restr s := rfl

/-- Composing two local homeomorphisms, by restricting to the maximal domain where their
composition is well defined. -/
protected def trans (e : local_homeomorph α β) (e' : local_homeomorph β γ) : local_homeomorph α γ :=
  local_homeomorph.trans' (e.symm.restr_open e'.source e'.open_source).symm
    (e'.restr_open e.target e.open_target) (by simp [inter_comm])

lemma trans_to_local_equiv (e : local_homeomorph α β) (e' : local_homeomorph β γ) :
  (e.trans e').to_local_equiv = e.to_local_equiv.trans e'.to_local_equiv := rfl

lemma trans_source (e : local_homeomorph α β) (e' : local_homeomorph β γ) :
  (e.trans e').source = e.source ∩ e.to_fun ⁻¹' e'.source :=
local_equiv.trans_source e.to_local_equiv e'.to_local_equiv

lemma trans_source' (e : local_homeomorph α β) (e' : local_homeomorph β γ) :
  (e.trans e').source = e.source ∩ e.to_fun ⁻¹' (e.target ∩ e'.source) :=
local_equiv.trans_source' e.to_local_equiv e'.to_local_equiv

lemma trans_source'' (e : local_homeomorph α β) (e' : local_homeomorph β γ) :
  (e.trans e').source = e.inv_fun '' (e.target ∩ e'.source) :=
local_equiv.trans_source'' e.to_local_equiv e'.to_local_equiv

@[simp]lemma trans_to_fun (e : local_homeomorph α β) (e' : local_homeomorph β γ) :
  (e.trans e').to_fun = e'.to_fun ∘ e.to_fun := rfl

lemma trans_symm_eq (e : local_homeomorph α β) (e' : local_homeomorph β γ) :
  (e.trans e').symm = e'.symm.trans e.symm :=
by cases e; cases e'; refl

lemma trans_assoc (e : local_homeomorph α β) (e' : local_homeomorph β γ) (e'' : local_homeomorph γ δ) :
  (e.trans e').trans e'' = e.trans (e'.trans e'') :=
eq_of_local_equiv_eq $ local_equiv.trans_assoc e.to_local_equiv e'.to_local_equiv e''.to_local_equiv

@[simp] lemma trans_refl (e : local_homeomorph α β) : e.trans (local_homeomorph.refl β) = e :=
eq_of_local_equiv_eq $ local_equiv.trans_refl e.to_local_equiv

@[simp] lemma refl_trans (e : local_homeomorph α β) : (local_homeomorph.refl α).trans e = e :=
eq_of_local_equiv_eq $ local_equiv.refl_trans e.to_local_equiv

lemma trans_refl_restr (e : local_homeomorph α β) (s : set β) :
  e.trans ((local_homeomorph.refl β).restr s) = e.restr (e.to_fun ⁻¹' s) :=
begin
  apply local_homeomorph.eq,
  { refl },
  { refl },
  { simp [e.preimage_interior, trans_source] }
end

lemma trans_refl_restr' (e : local_homeomorph α β) (s : set β) :
  e.trans ((local_homeomorph.refl β).restr s) = e.restr (e.source ∩ e.to_fun ⁻¹' s) :=
begin
  apply local_homeomorph.eq,
  { refl },
  { refl },
  { simp only [refl_source, interior_inter, restr_source, univ_inter, trans_source],
    rw [e.preimage_interior, interior_eq_of_open e.open_source, ← inter_assoc, inter_self] }
end

lemma restr_trans (e : local_homeomorph α β) (e' : local_homeomorph β γ) (s : set α) :
  (e.restr s).trans e' = (e.trans e').restr s :=
eq_of_local_equiv_eq $ local_equiv.restr_trans e.to_local_equiv e'.to_local_equiv (interior s)

lemma homeomorph_to_local_homeomorph_trans (e : homeomorph α β) (e' : homeomorph β γ) :
  (e.trans e').to_local_homeomorph = e.to_local_homeomorph.trans e'.to_local_homeomorph :=
eq_of_local_equiv_eq $ local_equiv.equiv_to_local_equiv_trans _ _

/-- `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. -/
def eq_on_source (e e' : local_homeomorph α β) : Prop :=
  local_equiv.eq_on_source e.to_local_equiv e'.to_local_equiv

/-- `eq_on_source` is an equivalence relation -/
instance : setoid (local_homeomorph α β) :=
{ r     := eq_on_source,
  iseqv := ⟨
    λe, (@local_equiv.eq_on_source_setoid α β).iseqv.1 _,
    λe e' h, (@local_equiv.eq_on_source_setoid α β).iseqv.2.1 h,
    λe e' e'' h h', (@local_equiv.eq_on_source_setoid α β).iseqv.2.2 h h'⟩ }

lemma eq_on_source_refl (e : local_homeomorph α β) : e ≈ e := setoid.refl _

/-- If two local homeomorphisms are equivalent, so are their inverses -/
lemma eq_on_source_symm (e e' : local_homeomorph α β) (h : e ≈ e') : e.symm ≈ e'.symm :=
local_equiv.eq_on_source_symm _ _ h

/-- Two equivalent local homeomorphisms have the same source -/
lemma source_eq_of_eq_on_source (e e' : local_homeomorph α β) (h : e ≈ e') : e.source = e'.source :=
h.1

/-- Two equivalent local homeomorphisms have the same target -/
lemma target_eq_of_eq_on_source (e e' : local_homeomorph α β) (h : e ≈ e') : e.target = e'.target :=
(eq_on_source_symm e e' h).1

/-- Two equivalent local homeomorphisms have coinciding `to_fun` on the source -/
lemma to_fun_eq_of_eq_on_source (e e' : local_homeomorph α β) (h : e ≈ e') {x : α} (hx : x ∈ e.source) :
  e.to_fun x = e'.to_fun x :=
h.2 x hx

/-- Two equivalent local homeomorphisms have coinciding `inv_fun` on the target -/
lemma inv_fun_eq_of_eq_on_source (e e' : local_homeomorph α β) (h : e ≈ e') {x : β} (hx : x ∈ e.target) :
  e.inv_fun x = e'.inv_fun x :=
(eq_on_source_symm e e' h).2 x hx

/-- Composition of local homeomorphisms respects equivalence -/
lemma eq_on_source_trans (e e' : local_homeomorph α β) (f f' : local_homeomorph β γ)
  (he : e ≈ e') (hf : f ≈ f') : e.trans f ≈ e'.trans f' :=
begin
  change local_equiv.eq_on_source (e.trans f).to_local_equiv (e'.trans f').to_local_equiv,
  simp only [trans_to_local_equiv],
  apply local_equiv.eq_on_source_trans,
  exact he,
  exact hf
end

/-- Restriction of local homeomorphisms respects equivalence -/
lemma eq_on_source_restr (e e' : local_homeomorph α β) (he : e ≈ e') (s : set α) :
  e.restr s ≈ e'.restr s :=
local_equiv.eq_on_source_restr _ _ he _

/-- Composition of a local homeomorphism and its inverse is equivalent to the restriction of the
identity to the source -/
lemma trans_self_symm (e : local_homeomorph α β) :
  e.trans e.symm ≈ (local_homeomorph.refl α).restr e.source :=
begin
  change local_equiv.eq_on_source (e.trans e.symm).to_local_equiv
               ((local_homeomorph.refl α).restr e.source).to_local_equiv,
  rw [trans_to_local_equiv, restr_to_local_equiv' _ _ e.open_source],
  apply local_equiv.trans_self_symm
end

lemma trans_symm_self (e : local_homeomorph α β) :
  e.symm.trans e ≈ (local_homeomorph.refl β).restr e.target :=
e.symm.trans_self_symm

end local_homeomorph


















namespace manifold

local infixr  ` →ₕ `:100 := local_homeomorph.trans
open local_homeomorph

/- One could add to the definition of a structure groupoid the fact that the restriction of an
element of the groupoid still belongs to the groupoid. (This is in Kobayashi-Nomizu.)
I am not sure I want this, for instance on α × E where E is a vector space, and the groupoid is made
of functions respecting the fibers and linear in the fibers (so that a manifold over this groupoid
is naturally a vector bundle) I prefer that the members of the groupoid are always defined on
sets of the form s × E

The only nontrivial requirement is locality: if a local homeomorphisms belongs to the groupoid
around each point in its domain of definition, then it belongs to the groupoid. Without this
requirement, the composition of diffeomorphisms does not have to be a diffeomorphism.

We also require that being a member of the groupoid only depends on the values on the source, as
the other values are irrelevant.
-/
structure structure_groupoid (α : Type*) [topological_space α] :=
(members      : set (local_homeomorph α α))
(comp         : ∀e e' : local_homeomorph α α, e ∈ members → e' ∈ members → e →ₕ e' ∈ members)
(inv          : ∀e : local_homeomorph α α, e ∈ members → e.symm ∈ members)
(id_mem       : local_homeomorph.refl α ∈ members)
(locality     : ∀e : local_homeomorph α α, (∀x ∈ e.source, ∃s, ∃hs : is_open s,
                  x ∈ s ∧ e.restr s ∈ members) → e ∈ members)
(eq_on_source : ∀ e e' : local_homeomorph α α, e ∈ members → e' ≈ e → e' ∈ members)

@[reducible] instance {α : Type*} [topological_space α] :
  has_mem (local_homeomorph α α) (structure_groupoid α) :=
⟨λ(e : local_homeomorph α α) (G : structure_groupoid α), e ∈ G.members⟩

variable [topological_space α]

class manifold (G : structure_groupoid α) (β : Type*) [topological_space β] :=
(chart  : set (local_homeomorph β α))
(compat : ∀e e' : local_homeomorph β α, e ∈ chart → e' ∈ chart → e.symm →ₕ e' ∈ G)
(cover  : ∀x, ∃e : local_homeomorph β α, e ∈ chart ∧ x ∈ e.source)

structure diffeomorph (G : structure_groupoid α) (β : Type*) (γ : Type*)
  [topological_space β] [topological_space γ] [mβ : manifold G β] [mγ : manifold G γ]
  extends homeomorph β γ :=
(smooth_to_fun : ∀c : local_homeomorph β α, ∀c' : local_homeomorph γ α,
  c ∈ mβ.chart → c' ∈ mγ.chart → c.symm →ₕ to_homeomorph.to_local_homeomorph →ₕ c' ∈ G)

variables [topological_space β] [topological_space γ] [topological_space δ]
{G : structure_groupoid α} [manifold G β] [manifold G γ] [manifold G δ]

def diffeomorph.symm (e : diffeomorph G β γ) : diffeomorph G γ β :=
{ smooth_to_fun := begin
    assume c c' hc hc',
    have : (c'.symm →ₕ e.to_homeomorph.to_local_homeomorph →ₕ c).symm ∈ G :=
      G.inv _ (e.smooth_to_fun c' c hc' hc),
    rwa [trans_symm_eq, trans_symm_eq, symm_symm, trans_assoc]
      at this,
  end,
  ..e.to_homeomorph.symm}

def diffeomorph.trans (e : diffeomorph G β γ) (e' : diffeomorph G γ δ) : diffeomorph G β δ :=
{ smooth_to_fun := begin
    /- Let c and c' be two charts in β and δ. We want to show that e' ∘ e is smooth in these
    charts, around any point x. For this, let y = e (c⁻¹ x), and consider a chart g around y.
    Then g ∘ e ∘ c⁻¹ and c' ∘ e' ∘ g⁻¹ are both smooth as e and e' are diffeomorphisms, so
    their composition is smooth, and it coincides with c' ∘ e' ∘ e ∘ c⁻¹ around x. -/
    assume c c' hc hc',
    refine G.locality _ (λx hx, _),
    let f₁ := e.to_homeomorph.to_local_homeomorph,
    let f₂ := e'.to_homeomorph.to_local_homeomorph,
    let f  := (e.to_homeomorph.trans e'.to_homeomorph).to_local_homeomorph,
    have feq : f = f₁ →ₕ f₂ := homeomorph_to_local_homeomorph_trans _ _,
    -- define the chart g around y
    let y := (c.symm →ₕ f₁).to_fun x,
    rcases manifold.cover G y with ⟨g, ⟨hg1, hg2⟩⟩,
    let s := (c.symm →ₕ f₁).source ∩ (c.symm →ₕ f₁).to_fun ⁻¹' g.source,
    have open_s : is_open s,
      by apply (c.symm →ₕ f₁).continuous_to.preimage_open_of_open; apply open_source,
    have : x ∈ s,
    { split,
      { simp only [trans_source, preimage_univ, inter_univ, homeomorph.to_local_homeomorph_source],
        rw trans_source at hx,
        exact hx.1 },
      { exact hg2 } },
    refine ⟨s, open_s, ⟨this, _⟩⟩,
    let F₁ := (c.symm →ₕ f₁ →ₕ g) →ₕ (g.symm →ₕ f₂ →ₕ c'),
    have A : F₁ ∈ G := G.comp _ _ (e.smooth_to c g hc hg1) (e'.smooth_to g c' hg1 hc'),
    let F₂ := (c.symm →ₕ f →ₕ c').restr s,
    have : F₁ ≈ F₂ := calc
      F₁ ≈ c.symm →ₕ f₁ →ₕ (g →ₕ g.symm) →ₕ f₂ →ₕ c' : by simp [F₁, trans_assoc]
      ... ≈ c.symm →ₕ f₁ →ₕ ((local_homeomorph.refl γ).restr g.source) →ₕ f₂ →ₕ c' :
        by simp [eq_on_source_trans, trans_self_symm g]
      ... ≈ ((c.symm →ₕ f₁) →ₕ ((local_homeomorph.refl γ).restr g.source)) →ₕ (f₂ →ₕ c') :
        by simp [trans_assoc]
      ... ≈ ((c.symm →ₕ f₁).restr s) →ₕ (f₂ →ₕ c') : by simp [s, trans_refl_restr']
      ... ≈ ((c.symm →ₕ f₁) →ₕ (f₂ →ₕ c')).restr s : by simp [restr_trans]
      ... ≈ (c.symm →ₕ (f₁ →ₕ f₂) →ₕ c').restr s : by simp [eq_on_source_restr, trans_assoc]
      ... ≈ F₂ : by simp [F₂, feq],
    have : F₂ ∈ G := G.eq_on_source F₁ F₂ A (setoid.symm this),
    exact this
  end,
  ..homeomorph.trans e.to_homeomorph e'.to_homeomorph }


end manifold


#exit



/-- From here on, experiments -/

structure smoothness_class (α : Type*) [topological_space α] :=
(is_member   : set α → (α → α) → Prop)
(open_source : ∀U f, is_member U f → is_open U)
(restr       : ∀U V f, U ⊆ V → is_open U → is_member V f → is_member U f)
(comp        : ∀U V f g, is_member U f → is_member V g → (f '' U) ⊆ V → is_member U (g ∘ f))
(cont        : ∀U f, is_member U f → continuous_on f U)
(locality    : ∀U f (g : α → α), is_member U f → (∀x ∈ U, f x = g x) → is_member U g)
(id_mem      : is_member univ id)

/-- From a smoothness class, one can extract a groupoid by restricting to the elements in the
smoothness class that have an inverse in the same smoothness class. -/
def smoothness_class.to_groupoid {α : Type*} [topological_space α] (S : smoothness_class α) :
  groupoid α :=
{ is_member   := λU f, S.is_member U f ∧ (∃V g, S.is_member V g ∧ inv_on f g U V),
  open_source := λU f hUf, S.open_source U f hUf.1,
  restr       := λU V f hUV Uop hVf, begin
    split,
    apply S.restr U V f hUV Uop hVf.1,
    rcases hVf.2 with ⟨V', g, hg⟩,
    refine ⟨f '' U, g, _, _⟩,
    { apply S.restr _ V' g _ _ hg.1,
      apply inv_on },
  end,
  comp        := sorry,
  inv         := sorry,
  cont := sorry,
  locality := sorry,
  id_mem := ⟨S.id_mem, ⟨univ, id, ⟨S.id_mem, by simp [inv_on, left_inv_on, right_inv_on]⟩⟩⟩ }