The chain form under empty members and along an isomorphism

Two elementary transports of the chain form (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) used when the empty blow-ups of a run are deleted ([Kol07, 34.1]; cp1For_eraseEmpty in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1EraseEmpty): the chain form ignores members that are the unit ideal — for families related by an extension by empty members (ExtendsByEmpty) the two forms agree, the members through the point corresponding under the injection; and the chain form pulls back along a morphism whose stalk map at the point is an isomorphism (the converse of chainRelativeAt_of_comap_of_isIso_stalkMap, obtained from it along the inverse).

theorem Hironaka.Resolution.ExtendsByEmpty.mem_range_of_mem_support {X : AlgebraicGeometry.Scheme} {E₁ E₂ : X.DivisorFamily} {ι : E₁.ι → E₂.ι} (htop : ∀ j ∉ Set.range ι, E₂.component j = ⊤) {p : ↥X} {j : E₂.ι} (hj : p ∈ (E₂.component j).support) : j ∈ Set.range ι

The members through p of a family and of its extension by empty members correspond: a member of the extension through p is not the unit ideal, hence in the range of the injection.

theorem Hironaka.Resolution.chainRelativeAt_of_extendsByEmpty {X : AlgebraicGeometry.Scheme} {E₁ E₂ : X.DivisorFamily} (hext : AlgebraicGeometry.ExtendsByEmpty E₁ E₂) {I Γ : X.IdealSheafData} {p : ↥X} : ChainRelativeAt E₁ I Γ p ↔ ChainRelativeAt E₂ I Γ p

The chain form ignores empty members — for E₂ an extension of E₁ by unit members, the chain forms along Γ at p agree.

theorem Hironaka.Resolution.chainRelativeAt_comap_of_isIso_stalkMap {X Y : AlgebraicGeometry.Scheme} (φ : Y ⟶ X) [CategoryTheory.IsIso φ] {E : X.DivisorFamily} {I Γ : X.IdealSheafData} (q : ↥Y) (h : ChainRelativeAt E I Γ (φ q)) : ChainRelativeAt (E.comap φ) (I.comap φ) (Γ.comap φ) q

The chain form pulls back along a morphism whose stalk map at the point is an isomorphism — chainRelativeAt_of_comap_of_isIso_stalkMap applied to the inverse.