English
The trivial restriction-closed groupoid consists exactly of open partial homeomorphisms equivalent to restrictions of the identity to open sets.
Русский
Тривиальный ограниченно-закрытый группоид состоит из открытых частичных гомоморфизмов, эквивалентных ограничению тождества на открытых множествах.
LaTeX
$$$\\text{IdRestrGroupoid}(H) = \\{ e \\in \\text{OpenPartialHomeomorph}(H,H) \\mid \\exists s,h, e \\approx \\mathrm{OpenPartialHomeomorph.ofSet}(s,h) \\}$$$
Lean4
/-- The trivial restriction-closed groupoid, containing only open partial homeomorphisms equivalent
to the restriction of the identity to the various open subsets. -/
def idRestrGroupoid : StructureGroupoid H
where
members := {e | ∃ (s : Set H) (h : IsOpen s), e ≈ OpenPartialHomeomorph.ofSet s h}
trans' := by
rintro e e' ⟨s, hs, hse⟩ ⟨s', hs', hse'⟩
refine ⟨s ∩ s', hs.inter hs', ?_⟩
have := OpenPartialHomeomorph.EqOnSource.trans' hse hse'
rwa [OpenPartialHomeomorph.ofSet_trans_ofSet] at this
symm' := by
rintro e ⟨s, hs, hse⟩
refine ⟨s, hs, ?_⟩
rw [← ofSet_symm]
exact OpenPartialHomeomorph.EqOnSource.symm' hse
id_mem' := ⟨univ, isOpen_univ, by simp only [mfld_simps, refl]⟩
locality' := by
intro e h
refine ⟨e.source, e.open_source, by simp only [mfld_simps], ?_⟩
intro x hx
rcases h x hx with ⟨s, hs, hxs, s', hs', hes'⟩
have hes : x ∈ (e.restr s).source := by
rw [e.restr_source]
refine ⟨hx, ?_⟩
rw [hs.interior_eq]
exact hxs
simpa only [mfld_simps] using OpenPartialHomeomorph.EqOnSource.eqOn hes' hes
mem_of_eqOnSource' := by
rintro e e' ⟨s, hs, hse⟩ hee'
exact ⟨s, hs, Setoid.trans hee' hse⟩
