Transport of the chain form along a stalk isomorphism

The chain-relative form (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) is a statement about one stalk; it transports along a morphism whose stalk map at the point is an isomorphism — the pieces of the local cover of [Kol07, Theorem 105], openImmersionCoprods (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedClaimCoverTools): the form of I.comap φ along Γ.comap φ at q gives the form of I along Γ at φ q, with the coordinates pulled back along the inverse isomorphism and the same exponents. The members through q of the pulled-back family are the members through φ q (AlgebraicGeometry.mem_support_comap_iff_apply). Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Cover and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainExtendsByEmpty.

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

The chain-relative form transports along a morphism whose stalk map at the point is an isomorphism.