The homOfPullbackEq calculus across two models

Generic identities for the morphism of closed subspaces IdealSheaf.homOfPullbackEq f hf h : Sp(J') → Sp(J) over an analytic map f between standard-model manifolds of possibly different dimensions with J' = f^* J (ClosedSubspaceHom.lean), for the padding identity at the coproduct of the pieces (CoproductPadIdentity.lean; the weak commutation with closed embeddings, [Kol07, 34.4]); none of them mentions an embedding datum or a blow-up run:

• IdealSheaf.sigmaOf_mono: the coproduct ideal sheaf is monotone summand by summand;
• IsClosedSubmanifold.pullback_idealSheaf_diffeomorph_of_eq: the cast form (k = n) of comap_idealSheaf_of_isLocalDiffeomorph — the ideal sheaf of a closed submanifold pulled back along a diffeomorphism across a model cast is the ideal sheaf of its preimage;
• comap_homOfPullbackEq_comap_toAnalyticSpaceι_idealSheaf: the member transport — when the ideal sheaf of a closed submanifold Y of the target pulls back along f to that of Y', the closed subspaces of Sp(J) and Sp(J') they trace correspond under homOfPullbackEq;
• IdealSheaf.homOfPullbackEq_comp_fun: homOfPullbackEq along a composite is the composite of the homOfPullbackEqs (the raw-function, two-models-per-step form of homOfPullbackEq_comp, QuotientHomSquares.lean);
• quotientMap_toSpaceHom_comp_homOfPullbackEq: the quotient square — for σ₁ ∘ f = g ∘ σ₂ on the ambient manifolds with K₂ = f^* K₁ and J₂ = g^* J₁, the quotient maps along Sp(σᵢ) commute with the homOfPullbackEqs along f and g (the mechanism of localResolutionHomOn_comp_map, LocalResolutionOn.lean: Hom.ext_of_comp_quotientι, quotientMap_comp_quotientι, homOfPullbackEq_comp_toAnalyticSpaceι, ofManifoldHom_comp).

Not in the sources; bookkeeping.

theorem Manifold.IdealSheaf.sigmaOf_mono {𝕜 : Type} [RCLike 𝕜] {σ : Type u} [Countable σ] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (N : σ → AnalyticManifold 𝕜 E) {J K : (i : σ) → (N i).IdealSheaf} (h : ∀ (i : σ), J i ≤ K i) : sigmaOf N J ≤ sigmaOf N K

IdealSheaf.sigmaOf is monotone summand by summand (stalkwise, through stalkIdeal_sigmaOf_mk and Ideal.map_mono).

theorem Manifold.IsClosedSubmanifold.pullback_idealSheaf_diffeomorph_of_eq {𝕜 : Type} [RCLike 𝕜] {k n : ℕ} (hk : k = n) {M : AnalyticManifold 𝕜 (Fin k → 𝕜)} {M' : AnalyticManifold 𝕜 (Fin n → 𝕜)} (G : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin k → 𝕜)) M'.carrier M.carrier ⊤) {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin k → 𝕜)) Y c) {Y' : Set M'.carrier} (hY' : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) Y' c) (hYY' : ⇑G ⁻¹' Y = Y') : IdealSheaf.pullback ⇑G ⋯ hY.idealSheaf = hY'.idealSheaf

The cast form of comap_idealSheaf_of_isLocalDiffeomorph: the ideal sheaf of a closed submanifold pulled back along a DIFFEOMORPHISM across a model cast k = n is the ideal sheaf of its preimage.

theorem Hironaka.Manifold.comap_homOfPullbackEq_comap_toAnalyticSpaceι_idealSheaf {𝕜 : Type} [RCLike 𝕜] {n k : ℕ} {A : AnalyticManifold 𝕜 (Fin k → 𝕜)} {A' : AnalyticManifold 𝕜 (Fin n → 𝕜)} (f : A'.carrier → A.carrier) (hf : ContMDiff (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin k → 𝕜)) ⊤ f) {J : A.IdealSheaf} {J' : A'.IdealSheaf} (h : J' = Manifold.IdealSheaf.pullback f hf J) {Y : Set A.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin k → 𝕜)) Y c) {Y' : Set A'.carrier} {c' : ℕ} (hY' : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) Y' c') (hYY : Manifold.IdealSheaf.pullback f hf hY.idealSheaf = hY'.idealSheaf) : (AnalyticSpace.ClosedSubspace.comap hY.idealSheaf J.toAnalyticSpaceι).comap (Manifold.IdealSheaf.homOfPullbackEq f hf h) = AnalyticSpace.ClosedSubspace.comap hY'.idealSheaf J'.toAnalyticSpaceι

The member transport along homOfPullbackEq: for J' = f^* J and a member Y of the target whose ideal sheaf pulls back along f to the ideal sheaf of a member Y' of the source, the closed subspace of Sp(J) traced by Y pulls back along homOfPullbackEq f to the closed subspace of Sp(J') traced by Y' (comap_comp_hom, homOfPullbackEq_comp_toAnalyticSpaceι, comap_ofManifoldHom_eq_pullback).

theorem Manifold.IdealSheaf.homOfPullbackEq_comp_fun {𝕜 : Type} [RCLike 𝕜] {n₁ n₂ n₃ : ℕ} {A₁ : AnalyticManifold 𝕜 (Fin n₁ → 𝕜)} {A₂ : AnalyticManifold 𝕜 (Fin n₂ → 𝕜)} {A₃ : AnalyticManifold 𝕜 (Fin n₃ → 𝕜)} (f₁ : A₁.carrier → A₂.carrier) (hf₁ : ContMDiff (modelWithCornersSelf 𝕜 (Fin n₁ → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n₂ → 𝕜)) ⊤ f₁) (f₂ : A₂.carrier → A₃.carrier) (hf₂ : ContMDiff (modelWithCornersSelf 𝕜 (Fin n₂ → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n₃ → 𝕜)) ⊤ f₂) {J₁ : A₁.IdealSheaf} {J₂ : A₂.IdealSheaf} {J₃ : A₃.IdealSheaf} (h₁ : J₁ = pullback f₁ hf₁ J₂) (h₂ : J₂ = pullback f₂ hf₂ J₃) (h₁₂ : J₁ = pullback (f₂ ∘ f₁) ⋯ J₃) : CategoryTheory.CategoryStruct.comp (homOfPullbackEq f₁ hf₁ h₁) (homOfPullbackEq f₂ hf₂ h₂) = homOfPullbackEq (f₂ ∘ f₁) ⋯ h₁₂

The raw-function form of homOfPullbackEq_comp (QuotientHomSquares.lean), any two models per step: homOfPullbackEq along a composite is the composite of the homOfPullbackEqs.

theorem Hironaka.Manifold.quotientMap_toSpaceHom_comp_homOfPullbackEq {𝕜 : Type} [RCLike 𝕜] {n k : ℕ} {M₁ N₁ : AnalyticManifold 𝕜 (Fin k → 𝕜)} {M₂ N₂ : AnalyticManifold 𝕜 (Fin n → 𝕜)} (σ₁ : AnalyticMap M₁ N₁) (σ₂ : AnalyticMap M₂ N₂) (f : M₂.carrier → M₁.carrier) (hf : ContMDiff (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin k → 𝕜)) ⊤ f) (g : N₂.carrier → N₁.carrier) (hg : ContMDiff (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin k → 𝕜)) ⊤ g) (hcomm : ⇑σ₁ ∘ f = g ∘ ⇑σ₂) {K₁ : M₁.IdealSheaf} {J₁ : N₁.IdealSheaf} (c₁ : AnalyticSpace.QuotientSpace.Compat (↑(AnalyticSpace.toSpaceHom (ContinuousLinearEquiv.refl 𝕜 (Fin k → 𝕜)) σ₁)) K₁ J₁) {K₂ : M₂.IdealSheaf} {J₂ : N₂.IdealSheaf} (c₂ : AnalyticSpace.QuotientSpace.Compat (↑(AnalyticSpace.toSpaceHom (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) σ₂)) K₂ J₂) (hK : K₂ = Manifold.IdealSheaf.pullback f hf K₁) (hJ : J₂ = Manifold.IdealSheaf.pullback g hg J₁) : CategoryTheory.CategoryStruct.comp (Manifold.IdealSheaf.homOfPullbackEq f hf hK) (AnalyticSpace.KLocallyRingedSpace.quotientMap (AnalyticSpace.toSpaceHom (ContinuousLinearEquiv.refl 𝕜 (Fin k → 𝕜)) σ₁) K₁ J₁ c₁) = CategoryTheory.CategoryStruct.comp (AnalyticSpace.KLocallyRingedSpace.quotientMap (AnalyticSpace.toSpaceHom (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) σ₂) K₂ J₂ c₂) (Manifold.IdealSheaf.homOfPullbackEq g hg hJ)

The generic QUOTIENT SQUARE (the mechanism of localResolutionHomOn_comp_map, LocalResolutionOn.lean): for σ₁ ∘ f = g ∘ σ₂ on the ambient manifolds (any two models), with K₂ = f^* K₁ and J₂ = g^* J₁, the quotient maps along Sp(σᵢ) commute with the homOfPullbackEqs along f and g.