English
The trivial groupoid contains only the identity map (and maps with empty source).
Русский
Тривиальный группоида содержит только тождественный отображатель (и отображения с пустым источником).
LaTeX
$$def idGroupoid (H) : StructureGroupoid H$$
Lean4
/-- The trivial groupoid, containing only the identity (and maps with empty source, as this is
necessary from the definition). -/
def idGroupoid (H : Type u) [TopologicalSpace H] : StructureGroupoid H
where
members := {OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}
trans' e e' he
he' := by
rcases he with he | he
· simpa only [mem_singleton_iff.1 he, refl_trans]
· have : (e ≫ₕ e').source ⊆ e.source := sep_subset _ _
rw [he] at this
have : e ≫ₕ e' ∈ {e : OpenPartialHomeomorph H H | e.source = ∅} := eq_bot_iff.2 this
exact (mem_union _ _ _).2 (Or.inr this)
symm' e
he := by
rcases (mem_union _ _ _).1 he with E | E
· simp [mem_singleton_iff.mp E]
· right
simpa only [e.toPartialEquiv.image_source_eq_target.symm, mfld_simps] using E
id_mem' := mem_union_left _ rfl
locality' e
he := by
rcases e.source.eq_empty_or_nonempty with h | h
· right
exact h
· left
rcases h with ⟨x, hx⟩
rcases he x hx with ⟨s, open_s, xs, hs⟩
have x's : x ∈ (e.restr s).source := by
rw [restr_source, open_s.interior_eq]
exact ⟨hx, xs⟩
rcases hs with hs | hs
· replace hs : OpenPartialHomeomorph.restr e s = OpenPartialHomeomorph.refl H := by simpa only using hs
have : (e.restr s).source = univ := by
rw [hs]
simp
have : e.toPartialEquiv.source ∩ interior s = univ := this
have : univ ⊆ interior s := by
rw [← this]
exact inter_subset_right
have : s = univ := by rwa [open_s.interior_eq, univ_subset_iff] at this
simpa only [this, restr_univ] using hs
· exfalso
rw [mem_setOf_eq] at hs
rwa [hs] at x's
mem_of_eqOnSource' e e' he
he'e := by
rcases he with he | he
· left
have : e = e' := by
refine eq_of_eqOnSource_univ (Setoid.symm he'e) ?_ ?_ <;> rw [Set.mem_singleton_iff.1 he] <;> rfl
rwa [← this]
· right
have he : e.toPartialEquiv.source = ∅ := he
rwa [Set.mem_setOf_eq, EqOnSource.source_eq he'e]
