English
If G is closed under restriction, then the property IsLocalStructomorphWithinAt G is a LocalInvariantProp for G, i.e., it is stable under localization and composition within the groupoid structure.
Русский
Если G замыкается на ограничение, то свойство IsLocalStructomorphWithinAt G является локальным инвариантным свойством для G, то есть сохраняется локализация и композиция внутри группы.
LaTeX
$$$ [ClosedUnderRestriction\ G] : LocalInvariantProp G G (IsLocalStructomorphWithinAt G).$$$
Lean4
/-- For a groupoid `G` which is `ClosedUnderRestriction`, being a local structomorphism is a local
invariant property. -/
theorem isLocalStructomorphWithinAt_localInvariantProp [ClosedUnderRestriction G] :
LocalInvariantProp G G (IsLocalStructomorphWithinAt G) :=
{ is_local := by
intro s x u f hu hux
constructor
· rintro h hx
rcases h hx.1 with ⟨e, heG, hef, hex⟩
have : s ∩ u ∩ e.source ⊆ s ∩ e.source := by mfld_set_tac
exact ⟨e, heG, hef.mono this, hex⟩
· rintro h hx
rcases h ⟨hx, hux⟩ with ⟨e, heG, hef, hex⟩
refine ⟨e.restr (interior u), ?_, ?_, ?_⟩
· exact closedUnderRestriction' heG isOpen_interior
· have : s ∩ u ∩ e.source = s ∩ (e.source ∩ u) := by mfld_set_tac
simpa only [this, interior_interior, hu.interior_eq, mfld_simps] using hef
· simp only [*, hu.interior_eq, mfld_simps]
right_invariance' := by
intro s x f e' he'G he'x h hx
have hxs : x ∈ s := by simpa only [e'.left_inv he'x, mfld_simps] using hx
rcases h hxs with ⟨e, heG, hef, hex⟩
refine ⟨e'.symm.trans e, G.trans (G.symm he'G) heG, ?_, ?_⟩
· intro y hy
simp only [mfld_simps] at hy
simp only [hef ⟨hy.1, hy.2.2⟩, mfld_simps]
· simp only [hex, he'x, mfld_simps]
congr_of_forall := by
intro s x f g hfgs _ h hx
rcases h hx with ⟨e, heG, hef, hex⟩
refine ⟨e, heG, ?_, hex⟩
intro y hy
rw [← hef hy, hfgs y hy.1]
left_invariance' := by
intro s x f e' he'G _ hfx h hx
rcases h hx with ⟨e, heG, hef, hex⟩
refine ⟨e.trans e', G.trans heG he'G, ?_, ?_⟩
· intro y hy
simp only [mfld_simps] at hy
simp only [hef ⟨hy.1, hy.2.1⟩, mfld_simps]
· simpa only [hex, hef ⟨hx, hex⟩, mfld_simps] using hfx }
