The disjoint union of ideal sheaves and of triples

The disjoint union of a family of triples ([Kol07, Warning 38]; the proof of [Kol07, Proposition 37]). The triples on disjoint unions of Hironaka.Manifold.FiniteSuccession.Functor.SigmaTriple are pull-backs of a global triple along sigmaDescMap; when the pieces have no common global triple (as for the local pieces of an embedded desingularization), the disjoint union of their ambient triples needs its ideal sheaf built: IdealSheaf.sigmaOf I, at a point of the i-th summand the pull-back of I i along the summand projection sigmaProj (analytic on the whole union, the local inverse of sigmaMk on the summand), glued by ofStalks along the clopen summands. Its restriction to each summand is I i (comap_sigmaMk_sigmaOf); reducedness and non-vanishing pass to it stalkwise. AnalyticTriple.sigmaOfEmpty is the disjoint union of triples with empty divisors, with its IsSigmaOf.

theorem Manifold.IdealSheaf.pullback_restrictOpens_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M P : AnalyticManifold 𝕜 E} (J : P.IdealSheaf) (φ φ' : AnalyticMap M P) (V : TopologicalSpace.Opens M.carrier) (h : Set.EqOn ⇑φ ⇑φ' ↑V) : AnalyticManifold.IdealSheaf.restrict (pullback ⇑φ ⋯ J) V = AnalyticManifold.IdealSheaf.restrict (pullback ⇑φ' ⋯ J) V

Two ideal-sheaf pull-backs along maps agreeing on an open agree there (pullback_pullback, pullback_congr).

theorem Manifold.IdealSheaf.stalkIdeal_eq_of_restrictOpens_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (K K' : M.IdealSheaf) (V : TopologicalSpace.Opens M.carrier) (h : K.restrict V = K'.restrict V) (p : M.carrier) (hp : p ∈ V) : stalkIdeal K p = stalkIdeal K' p

An ideal sheaf's stalk at a point of an open is determined by its restriction there (the germ map of the inclusion is bijective).

theorem Hironaka.Manifold.contMDiff_sigmaProj {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (i : σ) (x : (N i).carrier) : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (Manifold.sigmaProj N i x)

The projection onto a summand is analytic on the whole disjoint union: the identity on the summand, constant elsewhere (ContMDiff.sigmaDesc).

theorem Hironaka.Manifold.isLocalDiffeomorphAt_sigmaProj_mk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (i : σ) (x y : (N i).carrier) : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (Manifold.sigmaProj N i x) ((Manifold.sigmaMk N i) y)

The projection is a local analytic isomorphism at the points of its summand — the inverse of sigmaMkPartialDiffeomorph.

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.sigmaProjMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (i : σ) (x : (N i).carrier) : AnalyticMap (Manifold.sigmaManifold N) (N i)

The summand projection as an analytic map.

Equations

• Hironaka.Manifold.sigmaProjMap N i x = ⟨Manifold.sigmaProj N i x, ⋯⟩

noncomputable def Hironaka.Manifold.sigmaStalkIdeals {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (I : (i : σ) → (N i).IdealSheaf) (p : (Manifold.sigmaManifold N).carrier) : Ideal ↑((Manifold.structureSheaf 𝕜 E (Manifold.sigmaManifold N).carrier).presheaf.stalk p)

The stalk ideals of the disjoint union: at a point of the i-th summand, the pull-back of I i along the projection based at that point.

Equations

• Hironaka.Manifold.sigmaStalkIdeals N I p = (Manifold.IdealSheaf.pullback (Manifold.sigmaProj N p.fst p.snd) ⋯ (I p.fst)).stalkIdeal p

theorem Hironaka.Manifold.stalkIdeal_pullback_sigmaProj_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (I : (i : σ) → (N i).IdealSheaf) (i : σ) (x y z : (N i).carrier) : (Manifold.IdealSheaf.pullback (Manifold.sigmaProj N i x) ⋯ (I i)).stalkIdeal ((Manifold.sigmaMk N i) z) = (Manifold.IdealSheaf.pullback (Manifold.sigmaProj N i y) ⋯ (I i)).stalkIdeal ((Manifold.sigmaMk N i) z)

On the i-th summand the pull-backs along two projections agree.

theorem Hironaka.Manifold.hasLocalGenerators_sigmaStalkIdeals {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (I : (i : σ) → (N i).IdealSheaf) : Manifold.IdealSheaf.HasLocalGenerators (sigmaStalkIdeals N I)

The stalk ideals have local generators: those of the pull-back at the point, restricted to the clopen summand, where the pull-backs along the two projections agree.

noncomputable def Manifold.IdealSheaf.sigmaOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (I : (i : σ) → (N i).IdealSheaf) : (sigmaManifold N).IdealSheaf

([Kol07, Warning 38]) The disjoint union of ideal sheaves on the disjoint union of manifolds: at a point of the i-th summand the pull-back of I i along the summand projection (ofStalks).

Equations

• Manifold.IdealSheaf.sigmaOf N I = Manifold.IdealSheaf.ofStalks (Manifold.structureSheaf 𝕜 E (Manifold.sigmaManifold N).carrier) (Hironaka.Manifold.sigmaStalkIdeals N I) ⋯

theorem Manifold.IdealSheaf.stalkIdeal_sigmaOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (I : (i : σ) → (N i).IdealSheaf) (p : (sigmaManifold N).carrier) : stalkIdeal (sigmaOf N I) p = (pullback (sigmaProj N p.fst p.snd) ⋯ (I p.fst)).stalkIdeal p

theorem Manifold.IdealSheaf.stalkIdeal_sigmaOf_mk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (I : (i : σ) → (N i).IdealSheaf) (i : σ) (y : (N i).carrier) : stalkIdeal (sigmaOf N I) ((sigmaMk N i) y) = (pullback (sigmaProj N i y) ⋯ (I i)).stalkIdeal ((sigmaMk N i) y)

stalkIdeal_sigmaOf at a point of the i-th summand, spelled through sigmaMk.

theorem Manifold.IdealSheaf.comap_sigmaMk_sigmaOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (I : (i : σ) → (N i).IdealSheaf) (i : σ) : pullback ⇑(sigmaMk N i) ⋯ (sigmaOf N I) = I i

Its restriction to each summand is the summand's ideal sheaf (pullback_pullback, sigmaProj_mk, pullback_id_eq_self).

theorem Manifold.IdealSheaf.isReduced_sigmaOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (I : (i : σ) → (N i).IdealSheaf) (h : ∀ (i : σ), (I i).IsReduced) : (sigmaOf N I).IsReduced

Reducedness passes to the disjoint union (stalkwise, along the bijective germ maps of the projections).

theorem Manifold.IdealSheaf.isNonzeroEverywhere_sigmaOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) [FiniteDimensional 𝕜 E] (I : (i : σ) → (N i).IdealSheaf) (h : ∀ (i : σ), IsNonzeroEverywhere (I i)) : IsNonzeroEverywhere (sigmaOf N I)

Non-vanishing everywhere passes to the disjoint union (the order is preserved under the local isomorphism, ord_pullback_of_isLocalDiffeomorphAt).

noncomputable def Manifold.AnalyticTriple.sigmaOfEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (Ts : (i : σ) → AnalyticTriple ψ₀ (N i)) (_hF : ∀ (i : σ), (Ts i).F = HypersurfaceFamily.empty (N i).carrier) : AnalyticTriple ψ₀ (sigmaManifold N)

([Kol07, Warning 38]) The disjoint union of triples with empty divisors.

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.AnalyticTriple.isPullbackOf_sigmaOfEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (Ts : (i : σ) → AnalyticTriple ψ₀ (N i)) (hF : ∀ (i : σ), (Ts i).F = HypersurfaceFamily.empty (N i).carrier) (i : σ) : (Ts i).IsPullbackOf (sigmaOfEmpty N ψ₀ Ts hF) (sigmaMk N i)

Each triple is the pull-back of the disjoint union along its summand's inclusion.

theorem Manifold.AnalyticTriple.isSigmaOf_sigmaOfEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (Ts : (i : σ) → AnalyticTriple ψ₀ (N i)) (hF : ∀ (i : σ), (Ts i).F = HypersurfaceFamily.empty (N i).carrier) : (sigmaOfEmpty N ψ₀ Ts hF).IsSigmaOf Ts (sigmaMk N)

The disjoint union IS the disjoint union of the triples (isSigmaOf_sigma).

theorem Hironaka.Manifold.domBEDan_sigmaOfEmpty {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 (Fin n → 𝕜)) (Ts : (i : σ) → Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (N i)) (hF : ∀ (i : σ), (Ts i).F = Manifold.HypersurfaceFamily.empty (N i).carrier) (h : ∀ (i : σ), DomBEDan 𝕜 (Ts i)) : DomBEDan 𝕜 (Manifold.AnalyticTriple.sigmaOfEmpty N (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) Ts hF)

The class of bed is closed under disjoint unions with empty divisors: the divisor is empty and the ideal reduced (isReduced_sigmaOf).