The label coherence of the doubled datum

Kollár's agreement of the centres on the overlaps, (37.2) in [Kol07, Proposition 37, proof], for two runs. The coproduct member of label l of a datum D is traced on every piece (pieceTrace, CoproductGluedFamily.lean), and the gluing of the pieces' local resolutions needs these traces to be compatible along the transitions WITH THE IDENTITY LABELLING. The transitions come from the DOUBLED datum sumPadData D D — the datum padded to the left and to the right, read on one coproduct ambient — through the mixed-pair transition exists_mixedTransition_sumPadData (CoproductMixedTransition.lean), whose member clause is stated at the labels σ of the doubled run. A label l of D reaches the doubled run's stage set by TWO routes, lab₁ ∘ o₁.symm (the padding identity of the left copy, then the label embedding at inl of CoproductSumData.lean) and lab₂ ∘ o₂.symm (the right copy, inr), and the identity labelling of the traces needs the two routes to AGREE — on the labels whose member is not the unit ideal (⊤ in the closed-subspace order is the unit ideal, the EMPTY subspace, isUnit_iff; the off-range clauses of the label embeddings say nothing about a label with an empty member, so the routes need not agree there, and there the traces are all ⊤ and compatibility is trivial).

• exists_resIn_toFun_eq: the coproduct local resolution is covered by the summand inclusions resIn i (range_toFun_resIn, coe_sigmaCoordImage).
• exists_mem_support_comap_resIn_of_ne_top: a non-unit closed subspace of the coproduct local resolution has a point on some piece.
• sumLabelTrace: the ⊤-extended piece trace along a label embedding into a common label set, with its two evaluation lemmas — the families of the conjugation lemma of CoproductGluedFamilyCompat.lean.
• comap_sumInrResIn_sigmaMembers_ne_top_iff: the POINTWISE STEP — a stage of the doubled run has a non-empty trace on the inr copy iff on the inl copy: a point of one trace lies on a piece, its image in X lies in both piece domains (pieceDom_padAlongData), the mixed-pair transition at the same piece on both sides gives an isomorphism over a neighbourhood carrying the one trace to the other, and supports transfer along the inverse image (cosupport_comap).
• label_route_eq_of_ne_top: the two label routes agree on the non-trivial labels — the routes restricted to those labels are order embeddings of a finite linear order with equal ranges (OrderEmbedding.range_inj, Finite.to_wellFoundedLT; finiteness through finite_nonempty_totalTransformSeq).

No swap of the doubled ambient, no transport of the run, no non-emptiness of members is used anywhere. Not in the sources beyond Kollár's proof; bookkeeping.

theorem Manifold.IdealSheaf.ne_top_of_mem_support {X : AlgebraicGeometry.LocallyRingedSpace} {J : IdealSheaf X.𝒪} {z : ↑X.toTopCat} (hz : z ∈ J.support) : J ≠ ⊤

A point of the cosupport of an ideal sheaf witnesses that it is not the unit ideal (cosupport_top).

Four bookkeeping facts about the inverse image of ideal sheaves along a morphism of locally ringed spaces (QuotientSpace.comap), stated once here for this module and the modules above it: the unit ideal pulls back to the unit ideal, a non-unit inverse image comes from a non-unit ideal, a point of the cosupport witnesses a non-unit ideal, and an isomorphism preserves non-unit ideals (cosupport_comap: the cosupport of the inverse image is the preimage of the cosupport).

theorem AnalyticSpace.QuotientSpace.comap_top_idealSheaf {X' X : AlgebraicGeometry.LocallyRingedSpace} (φ : X' ⟶ X) : comap φ ⊤ = ⊤

The inverse image of the unit ideal is the unit ideal (its cosupport is the preimage of the empty set).

theorem AnalyticSpace.QuotientSpace.ne_top_of_comap_ne_top {X' X : AlgebraicGeometry.LocallyRingedSpace} (φ : X' ⟶ X) {J : Manifold.IdealSheaf X.𝒪} (h : comap φ J ≠ ⊤) : J ≠ ⊤

An ideal sheaf whose inverse image is not the unit ideal is not the unit ideal.

theorem AnalyticSpace.QuotientSpace.comap_ne_top_of_isIso {X' X : AlgebraicGeometry.LocallyRingedSpace} (φ : X' ⟶ X) [CategoryTheory.IsIso φ] {J : Manifold.IdealSheaf X.𝒪} (hJ : J ≠ ⊤) : comap φ J ≠ ⊤

Along an isomorphism the inverse image of a non-unit ideal sheaf is not the unit ideal — a point of the cosupport has a preimage (cosupport_comap).

theorem Hironaka.Manifold.LocalEmbeddingData.exists_resIn_toFun_eq {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (y : ↑↑(bed.localResolutionOn D.sigmaTriple ⋯ (D.ambImage W) ⋯).toPresheafedSpace) : ∃ (i : D.ι) (y' : ↑↑((D.embedding i).localResolution bed (W i) ⋯).toPresheafedSpace), AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resIn bed W hW hbed i) y' = y

The coproduct local resolution is covered by the summand inclusions — every point lies in the range of some resIn i (its image in the coproduct ambient lies in one summand of ambImage W = ⋃ i, sigmaMk i '' W i, coe_sigmaCoordImage; range_toFun_resIn).

theorem Hironaka.Manifold.LocalEmbeddingData.exists_mem_support_comap_resIn_of_ne_top {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (C : (bed.localResolutionOn D.sigmaTriple ⋯ (D.ambImage W) ⋯).ClosedSubspace) (hC : C ≠ ⊤) : ∃ (i : D.ι) (y' : ↑↑((D.embedding i).localResolution bed (W i) ⋯).toPresheafedSpace), y' ∈ (AnalyticSpace.QuotientSpace.comap (↑(D.resIn bed W hW hbed i)) C).support

A non-unit closed subspace of the coproduct local resolution has a point on some piece — the unit ideal is the closed subspace with empty support (isUnit_iff), and supports transfer along resIn i (cosupport_comap).

noncomputable def Hironaka.Manifold.LocalEmbeddingData.sumLabelTrace {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) {ι' Λ : Type u} [LinearOrder ι'] [LinearOrder Λ] (o : ι' ≃o D.sigmaIndex bed W hW) (lab : ι' ↪o Λ) (i : D.ι) (σ : Λ) : ((D.embedding i).localResolution bed (W i) ⋯).ClosedSubspace

The ⊤-extended piece trace along a label embedding — for a label σ of a common label set, the trace on piece i of the member of D carried by o from the label k with lab k = σ, and the unit ideal off the range of lab.

Equations

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

theorem Hironaka.Manifold.LocalEmbeddingData.sumLabelTrace_lab {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) {ι' Λ : Type u} [LinearOrder ι'] [LinearOrder Λ] (o : ι' ≃o D.sigmaIndex bed W hW) (lab : ι' ↪o Λ) (i : D.ι) (k : ι') : D.sumLabelTrace bed W hW hbed o lab i (lab k) = AnalyticSpace.QuotientSpace.comap (↑(D.resIn bed W hW hbed i)) (D.sigmaMembers bed W hW hbed (o k))

The extended trace at a label in the range is the trace of the member (lab is injective).

theorem Hironaka.Manifold.LocalEmbeddingData.sumLabelTrace_of_not_mem_range {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) {ι' Λ : Type u} [LinearOrder ι'] [LinearOrder Λ] (o : ι' ≃o D.sigmaIndex bed W hW) (lab : ι' ↪o Λ) (i : D.ι) {σ : Λ} (h : σ ∉ Set.range ⇑lab) : D.sumLabelTrace bed W hW hbed o lab i σ = ⊤

The extended trace at a label off the range is the unit ideal.

theorem Hironaka.Manifold.LocalEmbeddingData.comap_sumInrResIn_sigmaMembers_ne_top_iff {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (W₁ : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padLeftData D.n).embedding i).G).carrier) (hW₁ : ∀ (i : (D.padLeftData D.n).ι), IsCompact (closure ↑(W₁ i))) (W₂ : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padRightData D.n).embedding i).G).carrier) (hW₂ : ∀ (i : (D.padRightData D.n).ι), IsCompact (closure ↑(W₂ i))) (hpre : D.padPreimageOpens (Fin.castAddEmb D.n) W₁ = D.padPreimageOpens (Fin.natAddEmb D.n) W₂) (σ : (D.sumPadData D).sigmaIndex bed (D.sumPadOpens D W₁ W₂) ⋯) : AnalyticSpace.QuotientSpace.comap (↑(D.sumInrResIn D W₁ W₂ bed hW₁ hW₂ hbed)) ((D.sumPadData D).sigmaMembers bed (D.sumPadOpens D W₁ W₂) ⋯ hbed σ) ≠ ⊤ ↔ AnalyticSpace.QuotientSpace.comap (↑(D.sumInlResIn D W₁ W₂ bed hW₁ hW₂ hbed)) ((D.sumPadData D).sigmaMembers bed (D.sumPadOpens D W₁ W₂) ⋯ hbed σ) ≠ ⊤

A stage of the doubled run has a non-empty trace on the inr copy iff on the inl copy ((37.2) in [Kol07, Proposition 37, proof], on the diagonal pair) — THE POINTWISE STEP, with no labels: a point of one trace lies on a piece (exists_mem_support_comap_resIn_of_ne_top), its image lies in both piece domains (pieceDom_padAlongData and hpre), the mixed-pair transition at that piece on both sides carries the traces of every stage into each other over a neighbourhood of the point, and supports transfer along the inverse image (cosupport_comap; from the inr side through the inverse of the transition, comap_ne_top_of_isIso; the converse because a non-unit inverse image comes from a non-unit ideal, ne_top_of_comap_ne_top).

theorem Hironaka.Manifold.LocalEmbeddingData.label_route_eq_of_ne_top {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (W₁ : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padLeftData D.n).embedding i).G).carrier) (hW₁ : ∀ (i : (D.padLeftData D.n).ι), IsCompact (closure ↑(W₁ i))) (W₂ : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padRightData D.n).embedding i).G).carrier) (hW₂ : ∀ (i : (D.padRightData D.n).ι), IsCompact (closure ↑(W₂ i))) (V : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hV : ∀ (i : D.ι), IsCompact (closure ↑(V i))) (hpre₁ : D.padPreimageOpens (Fin.castAddEmb D.n) W₁ = V) (hpre₂ : D.padPreimageOpens (Fin.natAddEmb D.n) W₂ = V) (o₁ : (D.padLeftData D.n).sigmaIndex bed W₁ hW₁ ≃o D.sigmaIndex bed V hV) (ψ₁ : bed.localResolutionOn (D.padLeftData D.n).sigmaTriple ⋯ ((D.padLeftData D.n).ambImage W₁) ⋯ ⟶ bed.localResolutionOn D.sigmaTriple ⋯ (D.ambImage V) ⋯) (hψ₁ : CategoryTheory.IsIso ψ₁) (hmem₁ : ∀ (σp : (D.padLeftData D.n).sigmaIndex bed W₁ hW₁), AnalyticSpace.QuotientSpace.comap (↑ψ₁) (D.sigmaMembers bed V hV hbed (o₁ σp)) = (D.padLeftData D.n).sigmaMembers bed W₁ hW₁ hbed σp) (o₂ : (D.padRightData D.n).sigmaIndex bed W₂ hW₂ ≃o D.sigmaIndex bed V hV) (ψ₂ : bed.localResolutionOn (D.padRightData D.n).sigmaTriple ⋯ ((D.padRightData D.n).ambImage W₂) ⋯ ⟶ bed.localResolutionOn D.sigmaTriple ⋯ (D.ambImage V) ⋯) (hψ₂ : CategoryTheory.IsIso ψ₂) (hmem₂ : ∀ (σp : (D.padRightData D.n).sigmaIndex bed W₂ hW₂), AnalyticSpace.QuotientSpace.comap (↑ψ₂) (D.sigmaMembers bed V hV hbed (o₂ σp)) = (D.padRightData D.n).sigmaMembers bed W₂ hW₂ hbed σp) (lab₁ : (D.padLeftData D.n).sigmaIndex bed W₁ hW₁ ↪o (D.sumPadData D).sigmaIndex bed (D.sumPadOpens D W₁ W₂) ⋯) (hlab₁ : ∀ (k : (D.padLeftData D.n).sigmaIndex bed W₁ hW₁), AnalyticSpace.QuotientSpace.comap (↑(D.sumInlResIn D W₁ W₂ bed hW₁ hW₂ hbed)) ((D.sumPadData D).sigmaMembers bed (D.sumPadOpens D W₁ W₂) ⋯ hbed (lab₁ k)) = (D.padLeftData D.n).sigmaMembers bed W₁ hW₁ hbed k) (hlab₁' : ∀ σ ∉ Set.range ⇑lab₁, AnalyticSpace.QuotientSpace.comap (↑(D.sumInlResIn D W₁ W₂ bed hW₁ hW₂ hbed)) ((D.sumPadData D).sigmaMembers bed (D.sumPadOpens D W₁ W₂) ⋯ hbed σ) = ⊤) (lab₂ : (D.padRightData D.n).sigmaIndex bed W₂ hW₂ ↪o (D.sumPadData D).sigmaIndex bed (D.sumPadOpens D W₁ W₂) ⋯) (hlab₂ : ∀ (k : (D.padRightData D.n).sigmaIndex bed W₂ hW₂), AnalyticSpace.QuotientSpace.comap (↑(D.sumInrResIn D W₁ W₂ bed hW₁ hW₂ hbed)) ((D.sumPadData D).sigmaMembers bed (D.sumPadOpens D W₁ W₂) ⋯ hbed (lab₂ k)) = (D.padRightData D.n).sigmaMembers bed W₂ hW₂ hbed k) (hlab₂' : ∀ σ ∉ Set.range ⇑lab₂, AnalyticSpace.QuotientSpace.comap (↑(D.sumInrResIn D W₁ W₂ bed hW₁ hW₂ hbed)) ((D.sumPadData D).sigmaMembers bed (D.sumPadOpens D W₁ W₂) ⋯ hbed σ) = ⊤) (l : D.sigmaIndex bed V hV) (hl : D.sigmaMembers bed V hV hbed l ≠ ⊤) : lab₁ (o₁.symm l) = lab₂ (o₂.symm l)

The two label routes of the doubled datum agree on the non-trivial labels ((37.2) in [Kol07, Proposition 37, proof], on the diagonal pair (D, D)) — for a label l of D whose coproduct member is not the unit ideal, lab₁ (o₁.symm l) = lab₂ (o₂.symm l), where o₁, ψ₁ (resp. o₂, ψ₂) are the coproduct-level conjuncts of the padding identity read at the datum's reading opens V (exists_padIdentity_of_padPreimageOpens_eq: the order isomorphism of stage sets and the isomorphism of coproduct local resolutions carrying the members) and lab₁ (resp. lab₂) is the label embedding of the left (resp. right) copy into the doubled run with its two clauses (CoproductSumData.lean). The routes restricted to the non-trivial labels are order embeddings of a finite linear order; by comap_sumInrResIn_sigmaMembers_ne_top_iff each has its range inside the other's; equal ranges force equality (OrderEmbedding.range_inj). Off the non-trivial labels nothing is asserted: the label embeddings' witnesses are not determined at an empty member.