Transport of snc families along morphisms and locality for a given family

Bookkeeping of ClosedSubspace.IsSncFamily (Hironaka/AnalyticSpace/SncFamily.lean) under the pull-back of closed subspaces along morphisms of analytic spaces (QuotientSpace.comap, Hironaka/AnalyticSpace/QuotientMap.lean; Hironaka's inverse image of an analytic subspace, [Hir64, Ch. 0, §5, pp. 141–142]): the support of a pull-back is the preimage of the support; an isomorphism carries snc families and snc boundaries to snc families and snc boundaries; and, for a given global family, the snc condition is local on an open cover. The cover form for the predicate IsSncBoundary on a divisor alone is false — a nodal cubic is locally the union of two smooth branches without being the divisor of one global family of smooth members — so the gluing of families over a cover is a separate construction. The pointwise clause is isolated as IsSncAtIdeals on a family of ideals of a local ring and transported along a bijective ring homomorphism (IsSncAtIdeals.map_ringHom_of_bijective) and back along an isomorphism of CommRingCat (IsSncAtIdeals.of_map_isIso).

Used by Hironaka/Resolution/Analytic/Kol07Thm45/CoproductGluedFamily.lean, Hironaka/AnalyticSpace/SncBoundaryChart.lean and Hironaka/Resolution/Analytic/Kol07Thm45/Glue/OverFamilyPartner.lean.

def AnalyticSpace.IsSncAtIdeals {R : Type u_1} [CommRing R] [IsLocalRing R] {ι : Type u_2} (I : ι → Ideal R) : Prop

The pointwise clause of IsSncFamily on a family of ideals of a local ring: a regular system of parameters z and an injection c of the proper members into its indices with I j = (z (c j)).

Equations

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

theorem AnalyticSpace.IsSncAtIdeals.congr_ideals {R : Type u_1} [CommRing R] [IsLocalRing R] {ι : Type u_2} {I J : ι → Ideal R} (hIJ : I = J) (h : IsSncAtIdeals I) : IsSncAtIdeals J

theorem AnalyticSpace.IsSncAtIdeals.map_ne_top_iff_of_bijective {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (g : R →+* S) (hg : Function.Bijective ⇑g) (I : Ideal R) : Ideal.map g I ≠ ⊤ ↔ I ≠ ⊤

theorem AnalyticSpace.IsSncAtIdeals.map_ringHom_of_bijective {R : Type u_1} [CommRing R] [IsLocalRing R] {ι : Type u_2} {S : Type u_3} [CommRing S] [IsLocalRing S] {I : ι → Ideal R} (g : R →+* S) (hg : Function.Bijective ⇑g) (h : IsSncAtIdeals I) : IsSncAtIdeals fun (j : ι) => Ideal.map g (I j)

The pointwise clause transports along a bijective ring homomorphism.

theorem AnalyticSpace.IsSncAtIdeals.of_map_isIso {ι : Type u_2} {R S : CommRingCat} [IsLocalRing ↑R] (instS : IsLocalRing ↑S) (g : R ⟶ S) (hg : CategoryTheory.IsIso g) {I : ι → Ideal ↑R} (h : IsSncAtIdeals fun (j : ι) => Ideal.map (CommRingCat.Hom.hom g) (I j)) : IsSncAtIdeals I

The pointwise clause transports back along an isomorphism of commutative rings (the target's local-ring instance is passed explicitly: on a restricted space it is not found by search).

theorem AnalyticSpace.ClosedSubspace.isSncFamily_iff_isSncAtIdeals {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} (H : ι → X.ClosedSubspace) : IsSncFamily H ↔ (LocallyFinite fun (j : ι) => Manifold.IdealSheaf.support (H j)) ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsSncAtIdeals fun (j : ι) => Manifold.IdealSheaf.stalkIdeal (H j) x

theorem AnalyticSpace.ClosedSubspace.support_comap_eq_preimage {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : Y ⟶ X) (D : X.ClosedSubspace) : (QuotientSpace.comap (↑f) D).support = ↑f ⁻¹' Manifold.IdealSheaf.support D

The support of the pull-back of a closed subspace along a morphism is the preimage of its support (Hironaka's inverse image, [Hir64, Ch. 0, §5, pp. 141–142]; QuotientSpace.cosupport_comap). Named apart from HypersurfaceFamily.support_comap.

theorem AnalyticSpace.ClosedSubspace.isSncFamily_comap_of_isIso {K : Type} [RCLike K] {X Y : AnalyticSpace K} {ι : Type u} (f : Y ⟶ X) (hf : CategoryTheory.IsIso f) {H : ι → X.ClosedSubspace} (h : IsSncFamily H) : IsSncFamily fun (j : ι) => QuotientSpace.comap (↑f) (H j)

An isomorphism of analytic spaces carries an snc family of closed subspaces to an snc family ([Kol07, Definition 24] is pointwise): its stalk maps are ring isomorphisms, so regular systems of parameters go to regular systems and the members' principal stalk ideals to principal ideals (QuotientSpace.stalkIdeal_comap).

theorem AnalyticSpace.ClosedSubspace.isSncBoundary_comap_of_isIso {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : Y ⟶ X) (hf : CategoryTheory.IsIso f) {E : X.ClosedSubspace} (h : E.IsSncBoundary) : IsSncBoundary (QuotientSpace.comap (↑f) E)

An isomorphism of analytic spaces carries an snc boundary to an snc boundary: the family, the regular systems of parameters and the product clause transport along the stalk isomorphisms.

theorem AnalyticSpace.ClosedSubspace.isSncFamily_of_openCover {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {ι' : Type u_1} (U : ι' → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hU : ⋃ (i : ι'), ↑(U i) = Set.univ) (H : ι → X.ClosedSubspace) (h : ∀ (i : ι'), IsSncFamily fun (j : ι) => QuotientSpace.comap (↑(X.ofRestrict (U i))) (H j)) : IsSncFamily H

For a given global family the snc condition is local: local finiteness and the pointwise stalk clause are read on an open cover, along the inclusions X | Uᵢ ⟶ X of K-locally ringed spaces (KLocallyRingedSpace.ofRestrict), whose stalk maps are isomorphisms. No gluing of index sets is involved.