The disjoint union of the pieces' ambient triples

Kollár's local model is the disjoint union X' = ⊔ Uᵢ of an affine cover Kol07, Proposition 37, proof; in the library's form, with the pieces embedded in ambients: for a local embedding datum D over U ⊆ X, the disjoint union ⊔ᵢ Gᵢ of the pieces' ambients (sigmaAmbient) carries the disjoint union of their triples (Gᵢ, 𝓘ᵢ, ∅) (sigmaTriple, the ambientTriple of each piece summand by summand), a triple of the class of bed (domBEDan_sigmaTriple), each piece's triple the pull-back along its summand's inclusion (isPullbackOf_ambientTriple_sigmaTriple) — the input of the functor for the ambient blow-up factorization of the resolution (AmbientLift.lean).

Not in the sources; bookkeeping.

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.sigmaAmbient {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) : AnalyticManifold 𝕜 (Fin D.n → 𝕜)

The disjoint union of the pieces' ambients ([Kol07, Proposition 37, proof]).

Equations

• D.sigmaAmbient = Manifold.sigmaManifold fun (i : D.ι) => Hironaka.Manifold.pieceAmbient 𝕜 (D.embedding i).G

noncomputable def Hironaka.Manifold.LocalEmbeddingData.sigmaTriple {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin D.n → 𝕜)) D.sigmaAmbient

The disjoint union of the pieces' ambient triples (sigmaOfEmpty).

Equations

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

theorem Hironaka.Manifold.LocalEmbeddingData.isPullbackOf_ambientTriple_sigmaTriple {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (i : D.ι) : (D.embedding i).ambientTriple.IsPullbackOf D.sigmaTriple (Manifold.sigmaMk (fun (i : D.ι) => pieceAmbient 𝕜 (D.embedding i).G) i)

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

theorem Hironaka.Manifold.LocalEmbeddingData.domBEDan_sigmaTriple {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) : DomBEDan 𝕜 D.sigmaTriple

The disjoint union is a triple of the class of bed.