English
If two structure groupoids G1 and G2 on chain spaces exist, and G1 is compatible with open morphisms from G2 in a way that lifts local invariant properties, then the composed system forms a valid structure groupoid on the composition of the underlying manifolds.
Русский
Если существуют две структуры группоида G1 и G2 над связанных пространств, и G1 совместим с открытыми морфизмами из G2 так, что сохраняются локальные инвариантности, то полученная композиция образует корректный структуру группоида на композиции соответствующих многообразий.
LaTeX
$$$ \text{comp}(H : \forall e \in G_2, LiftPropOn (IsLocalStructomorphWithinAt G_1) e.source) \implies \text{HasGroupoid } H_3 G_1.$$$
Lean4
theorem comp (H : ∀ e ∈ G₂, LiftPropOn (IsLocalStructomorphWithinAt G₁) (e : H₂ → H₂) e.source) :
@HasGroupoid H₁ _ H₃ _ (ChartedSpace.comp H₁ H₂ H₃) G₁ :=
let _ := ChartedSpace.comp H₁ H₂ H₃
{
compatible := by
rintro _ _ ⟨e, he, f, hf, rfl⟩ ⟨e', he', f', hf', rfl⟩
apply G₁.locality
intro x hx
simp only [mfld_simps] at hx
have hxs : x ∈ f.symm ⁻¹' (e.symm ≫ₕ e').source := by simp only [hx, mfld_simps]
have hxs' : x ∈ f.target ∩ f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ e.symm ≫ₕ e' ⁻¹' f'.source) := by
simp only [hx, mfld_simps]
obtain ⟨φ, hφG₁, hφ, hφ_dom⟩ :=
LocalInvariantProp.liftPropOn_indep_chart (isLocalStructomorphWithinAt_localInvariantProp G₁)
(G₁.subset_maximalAtlas hf) (G₁.subset_maximalAtlas hf') (H _ (G₂.compatible he he')) hxs' hxs
simp_rw [← OpenPartialHomeomorph.coe_trans, OpenPartialHomeomorph.trans_assoc] at hφ
simp_rw [OpenPartialHomeomorph.trans_symm_eq_symm_trans_symm, OpenPartialHomeomorph.trans_assoc]
have hs : IsOpen (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source := (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').open_source
refine ⟨_, hs.inter φ.open_source, ?_, ?_⟩
· simp only [hx, hφ_dom, mfld_simps]
· refine G₁.mem_of_eqOnSource (closedUnderRestriction' hφG₁ hs) ?_
rw [OpenPartialHomeomorph.restr_source_inter]
refine OpenPartialHomeomorph.Set.EqOn.restr_eqOn_source (hφ.mono ?_)
mfld_set_tac }
