English
The toStructomorph construction is canonical and respects atlas memberships.
Русский
Конструкция toStructomorph канонична и сохраняет принадлежности атласа.
LaTeX
$$toStructomorph_proof$$
Lean4
/-- The composition of structomorphisms is a structomorphism. -/
def trans (e : Structomorph G M M') (e' : Structomorph G M' M'') : Structomorph G M M'' :=
{ Homeomorph.trans e.toHomeomorph e'.toHomeomorph with
mem_groupoid := by
/- Let c and c' be two charts in M and M''. 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 structomorphisms, so
their composition is smooth, and it coincides with c' ∘ e' ∘ e ∘ c⁻¹ around x. -/
intro c c' hc hc'
refine G.locality fun x hx ↦ ?_
let f₁ := e.toHomeomorph.toOpenPartialHomeomorph
let f₂ := e'.toHomeomorph.toOpenPartialHomeomorph
let f := (e.toHomeomorph.trans e'.toHomeomorph).toOpenPartialHomeomorph
have feq : f = f₁ ≫ₕ f₂ :=
Homeomorph.trans_toOpenPartialHomeomorph _
_
-- define the atlas g around y
let y := (c.symm ≫ₕ f₁) x
let g := chartAt (H := H) y
have hg₁ := chart_mem_atlas (H := H) y
have hg₂ := mem_chart_source (H := H) y
let s := (c.symm ≫ₕ f₁).source ∩ c.symm ≫ₕ f₁ ⁻¹' g.source
have open_s : IsOpen s := by apply (c.symm ≫ₕ f₁).continuousOn_toFun.isOpen_inter_preimage <;> apply open_source
have : x ∈ s := by
constructor
· simp only [f₁, trans_source, preimage_univ, inter_univ, Homeomorph.toOpenPartialHomeomorph_source]
rw [trans_source] at hx
exact hx.1
· exact hg₂
refine ⟨s, open_s, this, ?_⟩
let F₁ := (c.symm ≫ₕ f₁ ≫ₕ g) ≫ₕ g.symm ≫ₕ f₂ ≫ₕ c'
have A : F₁ ∈ G := G.trans (e.mem_groupoid c g hc hg₁) (e'.mem_groupoid g c' hg₁ hc')
let F₂ := (c.symm ≫ₕ f ≫ₕ c').restr s
have : F₁ ≈ F₂ :=
calc
F₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c' := by simp only [F₁, trans_assoc, _root_.refl]
_ ≈ c.symm ≫ₕ f₁ ≫ₕ ofSet g.source g.open_source ≫ₕ f₂ ≫ₕ c' :=
(EqOnSource.trans' (_root_.refl _)
(EqOnSource.trans' (_root_.refl _) (EqOnSource.trans' (self_trans_symm g) (_root_.refl _))))
_ ≈ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source g.open_source) ≫ₕ f₂ ≫ₕ c' := by simp only [trans_assoc, _root_.refl]
_ ≈ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c' := by rw [trans_of_set']
_ ≈ ((c.symm ≫ₕ f₁) ≫ₕ f₂ ≫ₕ c').restr s := by rw [restr_trans]
_ ≈ (c.symm ≫ₕ (f₁ ≫ₕ f₂) ≫ₕ c').restr s := by simp only [trans_assoc, _root_.refl]
_ ≈ F₂ := by simp only [F₂, feq, _root_.refl]
have : F₂ ∈ G := G.mem_of_eqOnSource A (Setoid.symm this)
exact this }
