Sheaf gluing for MeroGermOn (§6.6): the Čech H⁰ engine #
Unit: meromorphic-and-divisors (docs/design/meromorphic-and-divisors.md §4.4, proof plan §6.6).
MeroGermOn.exists_glue: compatible germ classes on an open cover glue to a class on the union (via the canonical repaired representativeholoRepr, whose pointwise rigidity —evalAt_restrict— makes the gluing elementary, no coherence lemma needed).MeroGermOn.glue_unique: the glued class is unique.
theorem
RS.MeroGermOn.exists_glue
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
{ι : Type u_2}
{W : ι → Set X}
(hW : ∀ (i : ι), IsOpen (W i))
(φ : (i : ι) → MeroGermOn X (W i))
(hcompat : ∀ (i j : ι), (restrict ⋯) (φ i) = (restrict ⋯) (φ j))
:
∃ (Φ : MeroGermOn X (⋃ (i : ι), W i)), ∀ (i : ι), (restrict ⋯) Φ = φ i
theorem
RS.MeroGermOn.glue_unique
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
{ι : Type u_2}
{W : ι → Set X}
(hW : ∀ (i : ι), IsOpen (W i))
{Φ Ψ : MeroGermOn X (⋃ (i : ι), W i)}
(h : ∀ (i : ι), (restrict ⋯) Φ = (restrict ⋯) Ψ)
: