English
If HasGroupoid M G holds, then chartAt H x lies in the maximal atlas.
Русский
Если HasGroupoid M G выполняется, то chartAt H x лежит в максимальном атласе.
LaTeX
$$$chartAt\ H\ x \in G.maximalAtlas M$$$
Lean4
/-- Changing coordinates between two elements of the maximal atlas gives rise to an element
of the structure groupoid. -/
theorem compatible_of_mem_maximalAtlas {e e' : OpenPartialHomeomorph M H} (he : e ∈ G.maximalAtlas M)
(he' : e' ∈ G.maximalAtlas M) : e.symm ≫ₕ e' ∈ G :=
by
refine G.locality fun x hx ↦ ?_
set f := chartAt (H := H) (e.symm x)
let s := e.target ∩ e.symm ⁻¹' f.source
have hs : IsOpen s := by apply e.symm.continuousOn_toFun.isOpen_inter_preimage <;> apply open_source
have xs : x ∈ s := by
simp only [s, f, mem_inter_iff, mem_preimage, mem_chart_source, and_true]
exact ((mem_inter_iff _ _ _).1 hx).1
refine ⟨s, hs, xs, ?_⟩
have A : e.symm ≫ₕ f ∈ G := (mem_maximalAtlas_iff.1 he f (chart_mem_atlas _ _)).1
have B : f.symm ≫ₕ e' ∈ G := (mem_maximalAtlas_iff.1 he' f (chart_mem_atlas _ _)).2
have C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G := G.trans A B
have D : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ≈ (e.symm ≫ₕ e').restr s :=
calc
(e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' = e.symm ≫ₕ (f ≫ₕ f.symm) ≫ₕ e' := by simp only [trans_assoc]
_ ≈ e.symm ≫ₕ ofSet f.source f.open_source ≫ₕ e' :=
(EqOnSource.trans' (refl _) (EqOnSource.trans' (self_trans_symm _) (refl _)))
_ ≈ (e.symm ≫ₕ ofSet f.source f.open_source) ≫ₕ e' := by rw [trans_assoc]
_ ≈ e.symm.restr s ≫ₕ e' := by rw [trans_of_set']; apply refl
_ ≈ (e.symm ≫ₕ e').restr s := by rw [restr_trans]
exact G.mem_of_eqOnSource C (Setoid.symm D)
