Ideal sheaves along an analytic isomorphism across the models

The second layer of the model transport (Hironaka/Resolution/Analytic/ModelTransport/). An analytic isomorphism g : N ≃ M between manifolds modelled on E' and E — for the main theorems the identity M.transport ψ → M of Hironaka/Resolution/Analytic/ModelTransport/Manifold.lean and the identities of its open subsets — carries every stalk-level notion of the analytic main theorems from M to N:

• the germ map 𝒪_{M, g b} → 𝒪_{N, b} is bijective at a local analytic isomorphism, whatever the two models (germMap_bijective_of_isLocalDiffeomorphAt', the two-model form of the lemma of Hironaka/Manifold/IdealSheaf/DerivLocality.lean), so it is a ring isomorphism of the stalks (Diffeomorph.stalkRingEquiv);
• the pull-back pullbackDiffeomorph g J := J.pullback g (IdealSheaf.pullback, which takes two models) has stalks the images of the stalks (stalkIdeal_pullbackDiffeomorph), support the preimage of the support, respects ⊤, ⊥ and products, is inverted by the pull-back along g⁻¹ and hence injective, and transports the pull-back along an analytic map across a square f ∘ g' = g ∘ f' (IsModelSquare, pullbackDiffeomorph_comap);
• the predicates of the vocabulary read on the stalks — IsNonzeroEverywhere, IsNonsingular, IsReduced, IsInvertible, HasOnlyNormalCrossingsWith and HasOnlyNormalCrossings (Hironaka's normal crossings at the stalk, [Hir64, Definition 2, p. 141]), IsNormalCrossingsDivisor (Bierstone–Milman's normal-crossings divisor, [BM97, Theorem 1.10]), ord — hold for the pull-back iff they hold for the ideal sheaf: each is a ring-theoretic statement about a stalk, carried by the stalk isomorphism (IsLocalRing.map_ringEquiv_maximalIdeal, ringKrullDim_eq_of_ringEquiv, Ideal.quotientEquiv, IsRegularLocalRing.of_ringEquiv, Ideal.IsRadical.comap, Ideal.comap_minimalPrimes_eq_of_surjective), and the points correspond under g; the simple locus regularLocus of the pull-back is the preimage of the simple locus (regularLocus_pullbackDiffeomorph);
• IdealSheaf.transport ψ J: an ideal sheaf on M read on M.transport ψ.

The pointwise bodies of HasOnlyNormalCrossingsWith and IsNormalCrossingsDivisor are transported on the ring side (exists_regularSystem_normalCrossings_map, exists_regularSystem_monomial_map); the two directions of each iff are the lemma at the stalk isomorphism and at its inverse. These are chart-independence statements: the predicates of the vocabulary are defined on stalks and see no coordinates.

theorem Hironaka.Manifold.germMap_bijective_of_isLocalDiffeomorphAt' {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) {b : N} (h : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ b) : Function.Bijective ⇑(Manifold.germMap φ hφ b)

The germ map of a local analytic isomorphism across the models is bijective: the germ map of a local inverse is a two-sided inverse (germMap_bijective_of_isLocalDiffeomorphAt of Hironaka/Manifold/IdealSheaf/DerivLocality.lean with the two models free; the same proof, the models only in its binders).

Ideals along a ring isomorphism

theorem Hironaka.Manifold.minimalPrimes_map_ringEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (e : R ≃+* S) (I : Ideal R) : (Ideal.map e I).minimalPrimes = Ideal.map e '' I.minimalPrimes

The minimal primes of the image of an ideal under a ring isomorphism are the images of its minimal primes (Ideal.comap_minimalPrimes_eq_of_surjective along the inverse).

theorem Hironaka.Manifold.mem_nonZeroDivisors_map_ringEquiv_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (e : R ≃+* S) (a : R) : e a ∈ nonZeroDivisors S ↔ a ∈ nonZeroDivisors R

A ring isomorphism preserves and reflects non-zero-divisors.

theorem Hironaka.Manifold.exists_regularSystem_normalCrossings_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (e : R ≃+* S) [IsLocalRing R] [IsLocalRing S] (I J : Ideal R) (h : ∃ (n : ℕ) (z : Fin n → R), (Ideal.span (Set.range z) = IsLocalRing.maximalIdeal R ∧ ↑n = ringKrullDim R) ∧ (∀ P ∈ I.minimalPrimes, ∃ (i : Fin n), P = Ideal.span {z i}) ∧ ∃ (s : Finset (Fin n)), J = Ideal.span (z '' ↑s)) : ∃ (n : ℕ) (z : Fin n → S), (Ideal.span (Set.range z) = IsLocalRing.maximalIdeal S ∧ ↑n = ringKrullDim S) ∧ (∀ P ∈ (Ideal.map e I).minimalPrimes, ∃ (i : Fin n), P = Ideal.span {z i}) ∧ ∃ (s : Finset (Fin n)), Ideal.map e J = Ideal.span (z '' ↑s)

The pointwise body of HasOnlyNormalCrossingsWith (Hironaka's normal crossings at the stalk, [Hir64, Definition 2, p. 141]: a regular system of parameters containing an equation of each minimal prime of I and equations for J) transports along a ring isomorphism of the stalks: the image of a regular system is a regular system (IsLocalRing.map_ringEquiv_maximalIdeal, ringKrullDim_eq_of_ringEquiv), the minimal primes correspond (minimalPrimes_map_ringEquiv).

theorem Hironaka.Manifold.exists_regularSystem_monomial_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (e : R ≃+* S) [IsLocalRing R] [IsLocalRing S] (J : Ideal R) (h : ∃ (n : ℕ) (z : Fin n → R) (α : Fin n → ℕ), (Ideal.span (Set.range z) = IsLocalRing.maximalIdeal R ∧ ↑n = ringKrullDim R) ∧ J = Ideal.span {∏ i : Fin n, z i ^ α i}) : ∃ (n : ℕ) (z : Fin n → S) (α : Fin n → ℕ), (Ideal.span (Set.range z) = IsLocalRing.maximalIdeal S ∧ ↑n = ringKrullDim S) ∧ Ideal.map e J = Ideal.span {∏ i : Fin n, z i ^ α i}

The pointwise body of IsNormalCrossingsDivisor (Bierstone–Milman's normal-crossings divisor at the stalk, [BM97, Theorem 1.10]: a monomial in a regular system of parameters) transports along a ring isomorphism of the stalks.

theorem Hironaka.Manifold.ideal_map_symm_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (e : R ≃+* S) (I : Ideal R) : Ideal.map e.symm (Ideal.map e I) = I

The image under the inverse of the image is the ideal.

The pull-back along an analytic isomorphism across the models

noncomputable def Diffeomorph.stalkRingEquiv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (b : N.carrier) : AnalyticManifold.IdealSheaf.stalkRing M (g b) ≃+* AnalyticManifold.IdealSheaf.stalkRing N b

The stalk isomorphism 𝒪_{M, g b} ≃+* 𝒪_{N, b} of an analytic isomorphism across the models: its germ map, bijective by germMap_bijective_of_isLocalDiffeomorphAt'.

Equations

• g.stalkRingEquiv b = RingEquiv.ofBijective (Manifold.germMap ⇑g ⋯ b) ⋯

theorem Diffeomorph.coe_stalkRingEquiv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (b : N.carrier) : ⇑(g.stalkRingEquiv b) = ⇑(Manifold.germMap ⇑g ⋯ b)

The stalk isomorphism is the germ map on points.

@[reducible, inline]

noncomputable abbrev AnalyticManifold.IdealSheaf.pullbackDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (J : M.IdealSheaf) : N.IdealSheaf

The pull-back of an ideal sheaf along an analytic isomorphism across the models (IdealSheaf.pullback, which takes two models).

Equations

• AnalyticManifold.IdealSheaf.pullbackDiffeomorph g J = Manifold.IdealSheaf.pullback ⇑g ⋯ J

theorem AnalyticManifold.IdealSheaf.stalkIdeal_pullbackDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (J : M.IdealSheaf) (b : N.carrier) : Manifold.IdealSheaf.stalkIdeal (pullbackDiffeomorph g J) b = Ideal.map (g.stalkRingEquiv b) (Manifold.IdealSheaf.stalkIdeal J (g b))

The stalk of the pull-back is the image of the stalk under the stalk isomorphism.

theorem AnalyticManifold.IdealSheaf.support_pullbackDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (J : M.IdealSheaf) : Manifold.IdealSheaf.support (pullbackDiffeomorph g J) = ⇑g ⁻¹' Manifold.IdealSheaf.support J

The support of the pull-back is the preimage of the support.

theorem AnalyticManifold.IdealSheaf.pullbackDiffeomorph_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) : pullbackDiffeomorph g ⊤ = ⊤

The unit ideal pulls back to the unit ideal.

theorem AnalyticManifold.IdealSheaf.pullbackDiffeomorph_mul {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (I J : M.IdealSheaf) : pullbackDiffeomorph g (I * J) = pullbackDiffeomorph g I * pullbackDiffeomorph g J

The pull-back of a product is the product of the pull-backs.

theorem AnalyticManifold.IdealSheaf.pullbackDiffeomorph_bot {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) : pullbackDiffeomorph g ⊥ = ⊥

The zero ideal sheaf pulls back to the zero ideal sheaf.

theorem AnalyticManifold.IdealSheaf.pullbackDiffeomorph_symm_pullbackDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (J : M.IdealSheaf) : pullbackDiffeomorph g.symm (pullbackDiffeomorph g J) = J

Pulling back along g and then along g⁻¹ is the identity.

theorem AnalyticManifold.IdealSheaf.pullbackDiffeomorph_injective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) : Function.Injective fun (J : M.IdealSheaf) => pullbackDiffeomorph g J

The pull-back along an analytic isomorphism is injective.

@[reducible, inline]

abbrev Hironaka.Manifold.IsModelSquare {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) {M' : AnalyticManifold 𝕜 E} {N' : AnalyticManifold 𝕜 E'} (g' : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N'.carrier M'.carrier ⊤) (f : AnalyticMap M' M) (f' : AnalyticMap N' N) : Prop

The square f ∘ g' = g ∘ f' of two analytic isomorphisms across the models and two analytic maps: the hypothesis of the transport lemmas of Hironaka/Resolution/Analytic/ModelTransport/Square.lean and SquareChart.lean.

Equations

• Hironaka.Manifold.IsModelSquare g g' f f' = ∀ (x : N'.carrier), f (g' x) = g (f' x)

theorem AnalyticManifold.IdealSheaf.pullbackDiffeomorph_comap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) {M' : AnalyticManifold 𝕜 E} {N' : AnalyticManifold 𝕜 E'} (g' : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N'.carrier M'.carrier ⊤) (f : AnalyticMap M' M) (f' : AnalyticMap N' N) (hsq : Hironaka.Manifold.IsModelSquare g g' f f') (J : M.IdealSheaf) : pullbackDiffeomorph g' (Manifold.IdealSheaf.pullback ⇑f ⋯ J) = Manifold.IdealSheaf.pullback ⇑f' ⋯ (pullbackDiffeomorph g J)

The pull-back along an analytic map (comap) transports along a square of analytic isomorphisms across the models.

theorem AnalyticManifold.IdealSheaf.isNonzeroEverywhere_pullbackDiffeomorph_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (J : M.IdealSheaf) : Manifold.IdealSheaf.IsNonzeroEverywhere (pullbackDiffeomorph g J) ↔ Manifold.IdealSheaf.IsNonzeroEverywhere J

IsNonzeroEverywhere along the isomorphism.

theorem AnalyticManifold.IdealSheaf.isNonsingular_pullbackDiffeomorph_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (J : M.IdealSheaf) : (pullbackDiffeomorph g J).IsNonsingular ↔ J.IsNonsingular

IsNonsingular (the regularity of the local rings 𝒪_x / J_x) along the isomorphism: the quotients are isomorphic rings (Ideal.quotientEquiv, IsRegularLocalRing.of_ringEquiv).

theorem AnalyticManifold.IdealSheaf.regularLocus_pullbackDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (J : M.IdealSheaf) : (pullbackDiffeomorph g J).regularLocus = ⇑g ⁻¹' J.regularLocus

The simple locus regularLocus along the isomorphism, the pointwise form of isNonsingular_pullbackDiffeomorph_iff: the quotients 𝒪_b / (g^*J)_b and 𝒪_{g b} / J_{g b} are isomorphic rings.

theorem AnalyticManifold.IdealSheaf.isReduced_pullbackDiffeomorph_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (J : M.IdealSheaf) : (pullbackDiffeomorph g J).IsReduced ↔ J.IsReduced

IsReduced along the isomorphism (Ideal.IsRadical.comap).

theorem AnalyticManifold.IdealSheaf.isInvertible_pullbackDiffeomorph_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (J : M.IdealSheaf) : Manifold.IdealSheaf.IsInvertible (pullbackDiffeomorph g J) ↔ Manifold.IdealSheaf.IsInvertible J

IsInvertible along the isomorphism: the generating non-zero-divisor is carried by the stalk isomorphism.

theorem AnalyticManifold.IdealSheaf.hasOnlyNormalCrossingsWith_pullbackDiffeomorph_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (E₀ D : M.IdealSheaf) : (pullbackDiffeomorph g E₀).HasOnlyNormalCrossingsWith (pullbackDiffeomorph g D) ↔ E₀.HasOnlyNormalCrossingsWith D

HasOnlyNormalCrossingsWith along the isomorphism.

theorem AnalyticManifold.IdealSheaf.hasOnlyNormalCrossings_pullbackDiffeomorph_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (E₀ : M.IdealSheaf) : (pullbackDiffeomorph g E₀).HasOnlyNormalCrossings ↔ E₀.HasOnlyNormalCrossings

HasOnlyNormalCrossings along the isomorphism.

theorem AnalyticManifold.IdealSheaf.isNormalCrossingsDivisor_pullbackDiffeomorph_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (J : M.IdealSheaf) : (pullbackDiffeomorph g J).IsNormalCrossingsDivisor ↔ J.IsNormalCrossingsDivisor

IsNormalCrossingsDivisor along the isomorphism.

theorem AnalyticManifold.IdealSheaf.ord_pullbackDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (J : M.IdealSheaf) (b : N.carrier) : Manifold.IdealSheaf.ord (pullbackDiffeomorph g J) b = Manifold.IdealSheaf.ord J (g b)

The order along the isomorphism (ord_pullback_of_isLocalDiffeomorphAt, which takes two models).

@[reducible, inline]

noncomputable abbrev AnalyticManifold.IdealSheaf.transport {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (J : M.IdealSheaf) : (M.transport ψ).IdealSheaf

An ideal sheaf on M read on the re-modelled M: the same sections, pulled back along the identity M.transport ψ → M.

Equations

• AnalyticManifold.IdealSheaf.transport ψ J = AnalyticManifold.IdealSheaf.pullbackDiffeomorph (M.transportDiffeomorph ψ).symm J