English
For a model with corners I, one defines a pregroupoid on H consisting of maps f for which I ∘ f ∘ I^{-1} is C^n on a suitable domain.
Русский
Для модели с углами I задаётся предгруппоид на H, состоящий из отображений f, для которых I ∘ f ∘ I^{-1} является C^n на подходящей области определения.
LaTeX
$$$\text{contDiffPregroupoid} : \text{Pregroupoid } H$$$
Lean4
/-- Given a model with corners `(E, H)`, we define the pregroupoid of `C^n` transformations of `H`
as the maps that are `C^n` when read in `E` through `I`. -/
def contDiffPregroupoid : Pregroupoid H
where
property f s := ContDiffOn 𝕜 n (I ∘ f ∘ I.symm) (I.symm ⁻¹' s ∩ range I)
comp {f g u v} hf hg _ _
_ := by
have : I ∘ (g ∘ f) ∘ I.symm = (I ∘ g ∘ I.symm) ∘ I ∘ f ∘ I.symm := by ext x; simp
simp only [this]
refine hg.comp (hf.mono fun x ⟨hx1, hx2⟩ ↦ ⟨hx1.1, hx2⟩) ?_
rintro x ⟨hx1, _⟩
simp only [mfld_simps] at hx1 ⊢
exact hx1.2
id_mem := by
apply ContDiffOn.congr contDiff_id.contDiffOn
rintro x ⟨_, hx2⟩
rcases mem_range.1 hx2 with ⟨y, hy⟩
rw [← hy]
simp only [mfld_simps]
locality {f u} _
H := by
apply contDiffOn_of_locally_contDiffOn
rintro y ⟨hy1, hy2⟩
rcases mem_range.1 hy2 with ⟨x, hx⟩
rw [← hx] at hy1 ⊢
simp only [mfld_simps] at hy1 ⊢
rcases H x hy1 with ⟨v, v_open, xv, hv⟩
have : I.symm ⁻¹' (u ∩ v) ∩ range I = I.symm ⁻¹' u ∩ range I ∩ I.symm ⁻¹' v :=
by
rw [preimage_inter, inter_assoc, inter_assoc]
congr 1
rw [inter_comm]
rw [this] at hv
exact ⟨I.symm ⁻¹' v, v_open.preimage I.continuous_symm, by simpa, hv⟩
congr {f g u} _ fg
hf := by
apply hf.congr
rintro y ⟨hy1, hy2⟩
rcases mem_range.1 hy2 with ⟨x, hx⟩
rw [← hx] at hy1 ⊢
simp only [mfld_simps] at hy1 ⊢
rw [fg _ hy1]
