# Documentation

## Smoothness of charts and local structomorphisms #

We show that the model with corners, charts, extended charts and their inverses are smooth, and that local structomorphisms are smooth with smooth inverses.

### Atlas members are smooth #

theorem contMDiff_model {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {n : ℕ∞} :
ContMDiff I () n I
theorem contMDiffOn_model_symm {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {n : ℕ∞} :
ContMDiffOn () I n (I.symm) ()
theorem contMDiffOn_of_mem_maximalAtlas {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {e : } {n : ℕ∞} (h : ) :
ContMDiffOn I I n (e) e.source

An atlas member is C^n for any n.

theorem contMDiffOn_symm_of_mem_maximalAtlas {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {e : } {n : ℕ∞} (h : ) :
ContMDiffOn I I n (e.symm) e.target

The inverse of an atlas member is C^n for any n.

theorem contMDiffAt_of_mem_maximalAtlas {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {e : } {x : M} {n : ℕ∞} (h : ) (hx : x e.source) :
ContMDiffAt I I n (e) x
theorem contMDiffAt_symm_of_mem_maximalAtlas {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {e : } {n : ℕ∞} {x : H} (h : ) (hx : x e.target) :
ContMDiffAt I I n (e.symm) x
theorem contMDiffOn_chart {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} {n : ℕ∞} :
ContMDiffOn I I n ((chartAt H x)) (chartAt H x).source
theorem contMDiffOn_chart_symm {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} {n : ℕ∞} :
ContMDiffOn I I n ((chartAt H x).symm) (chartAt H x).target
theorem contMDiffAt_extend {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {e : } {n : ℕ∞} {x : M} (he : ) (hx : x e.source) :
ContMDiffAt I () n ((e.extend I)) x
theorem contMDiffAt_extChartAt' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} {n : ℕ∞} {x' : M} (h : x' (chartAt H x).source) :
ContMDiffAt I () n (()) x'
theorem contMDiffAt_extChartAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} {n : ℕ∞} :
ContMDiffAt I () n (()) x
theorem contMDiffOn_extChartAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} {n : ℕ∞} :
ContMDiffOn I () n (()) (chartAt H x).source
theorem contMDiffOn_extend_symm {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {e : } {n : ℕ∞} (he : ) :
ContMDiffOn () I n ((e.extend I).symm) (I '' e.target)
theorem contMDiffOn_extChartAt_symm {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {n : ℕ∞} (x : M) :
ContMDiffOn () I n (().symm) ().target
theorem contMDiffOn_of_mem_contDiffGroupoid {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {n : ℕ∞} {e' : } (h : e' ) :
ContMDiffOn I I n (e') e'.source

An element of contDiffGroupoid ⊤ I is C^n for any n.

### Smoothness of (local) structomorphisms #

theorem isLocalStructomorphOn_contDiffGroupoid_iff_aux {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {M' : Type u_7} [] [ChartedSpace H M'] [IsM' : ] {f : } (hf : ChartedSpace.LiftPropOn ().IsLocalStructomorphWithinAt (f) f.source) :
SmoothOn I I (f) f.source
theorem isLocalStructomorphOn_contDiffGroupoid_iff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {M' : Type u_7} [] [ChartedSpace H M'] [IsM' : ] (f : ) :
ChartedSpace.LiftPropOn ().IsLocalStructomorphWithinAt (f) f.source SmoothOn I I (f) f.source SmoothOn I I (f.symm) f.target

Let M and M' be smooth manifolds with the same model-with-corners, I. Then f : M → M' is a local structomorphism for I, if and only if it is manifold-smooth on the domain of definition in both directions.