English
From a Pregroupoid, construct a StructureGroupoid whose members are OpenPartialHomeomorphs whose properties are stable under composition.
Русский
Из pregrouопoid строится StructureGroupoid с элементами OpenPartialHomeomorph, сохраняющими свойства при композиции.
LaTeX
$$def groupoid (PG : Pregroupoid H) : StructureGroupoid H$$
Lean4
/-- Construct a groupoid of partial homeos for which the map and its inverse have some property,
from a pregroupoid asserting that this property is stable under composition. -/
def groupoid (PG : Pregroupoid H) : StructureGroupoid H
where
members := {e : OpenPartialHomeomorph H H | PG.property e e.source ∧ PG.property e.symm e.target}
trans' e e' he
he' := by
constructor
· apply PG.comp he.1 he'.1 e.open_source e'.open_source
apply e.continuousOn_toFun.isOpen_inter_preimage e.open_source e'.open_source
· apply PG.comp he'.2 he.2 e'.open_target e.open_target
apply e'.continuousOn_invFun.isOpen_inter_preimage e'.open_target e.open_target
symm' _ he := ⟨he.2, he.1⟩
id_mem' := ⟨PG.id_mem, PG.id_mem⟩
locality' e
he := by
constructor
· refine PG.locality e.open_source fun x xu ↦ ?_
rcases he x xu with ⟨s, s_open, xs, hs⟩
refine ⟨s, s_open, xs, ?_⟩
convert hs.1 using 1
dsimp [OpenPartialHomeomorph.restr]
rw [s_open.interior_eq]
· refine PG.locality e.open_target fun x xu ↦ ?_
rcases he (e.symm x) (e.map_target xu) with ⟨s, s_open, xs, hs⟩
refine ⟨e.target ∩ e.symm ⁻¹' s, ?_, ⟨xu, xs⟩, ?_⟩
· exact ContinuousOn.isOpen_inter_preimage e.continuousOn_invFun e.open_target s_open
· rw [← inter_assoc, inter_self]
convert hs.2 using 1
dsimp [OpenPartialHomeomorph.restr]
rw [s_open.interior_eq]
mem_of_eqOnSource' e e' he
ee' := by
constructor
· apply PG.congr e'.open_source ee'.2
simp only [ee'.1, he.1]
· have A := EqOnSource.symm' ee'
apply PG.congr e'.symm.open_source A.2
convert he.2 using 1
rw [A.1, symm_toPartialEquiv, PartialEquiv.symm_source]
