Stabilisation along a coordinate inclusion

The proof of [Kol07, Theorem 36] increases n at will through a further embedding 𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ. This file supplies the closed-embedding data of the coordinate inclusions between the triples (𝔸ⁿ, I, ∅) and (𝔸ⁿ⁺ᵐ, I.map (coordInclFst n m), ∅) (and the second block likewise), the situation in which the principalization functor commutes with closed embeddings [Kol07, Theorem 35 (5)], and derives the stabilisation identity for BR_affine:

• affineSpaceTriple_closedEmbedding_coordInclFst and its second-block counterpart affineSpaceTriple_closedEmbedding_coordInclSnd: the coordinate inclusions are closed embeddings of triples (Triple.ClosedEmbedding): over k, the ideal of the larger triple is the image of the smaller one's, and the empty boundaries correspond;
• BR_affine_stabilize_of_BP_eq_pushforward: stabilising along 𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ does not change BR_affine, granted the identity BP (𝔸ⁿ⁺ᵐ, …) = (BP (𝔸ⁿ, …)).pushforward of Theorem 35 (5), which Hironaka.Resolution.Algebraic.Kol07.Thm36.Assembly supplies.

theorem Hironaka.Resolution.affineSpaceTriple_closedEmbedding_coordInclFst {k : Type u} [Field k] {n m : ℕ} (I : (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin n) k)).IdealSheafData) (hI : I.IsNonzeroEverywhere) (hI' : (I.map (coordInclFst n m)).IsNonzeroEverywhere) : (affineSpaceTriple k (n + m) (I.map (coordInclFst n m)) hI').ClosedEmbedding (affineSpaceTriple k n I hI) (coordInclFst n m)

The coordinate inclusion 𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ is a closed embedding of triples (𝔸ⁿ, I, ∅) ↪ (𝔸ⁿ⁺ᵐ, I.map (coordInclFst n m), ∅) in the sense of Triple.ClosedEmbedding, the situation of [Kol07, Theorem 35 (5)].

instance Hironaka.Resolution.isClosedImmersion_coordInclFst_affineSpaceTriple {k : Type u} [Field k] {n m : ℕ} (I : (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin n) k)).IdealSheafData) (hI : I.IsNonzeroEverywhere) (hI' : (I.map (coordInclFst n m)).IsNonzeroEverywhere) : AlgebraicGeometry.IsClosedImmersion (coordInclFst n m)

The coordinate inclusion, typed as a morphism between the ambients of the two affine-space triples (which are the affine spaces by definition), is a closed immersion: the instance isClosedImmersion_coordInclFst read at those types, so that the pushforward of sequences and [Kol07, Theorem 35 (5)] elaborate on the triples.

instance Hironaka.Resolution.isClosedImmersion_coordInclFst_affineSpaceTriple' {k : Type u} [Field k] {n m : ℕ} (I : (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin n) k)).IdealSheafData) (hI : I.IsNonzeroEverywhere) : AlgebraicGeometry.IsClosedImmersion (coordInclFst n m)

The same instance with the target read as the affine space itself.

theorem Hironaka.Resolution.BR_affine_stabilize_of_BP_eq_pushforward {k : Type u} [Field k] [CharZero k] {n m : ℕ} (I : (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin n) k)).IdealSheafData) (hI : I.IsNonzeroEverywhere) (hI' : (I.map (coordInclFst n m)).IsNonzeroEverywhere) (hBP : Sequence.BP (affineSpaceTriple k (n + m) (I.map (coordInclFst n m)) hI') = (Sequence.BP (affineSpaceTriple k n I hI)).pushforward (coordInclFst n m)) {X : AlgebraicGeometry.Scheme} (emb : X ⟶ AlgebraicGeometry.Spec ↧(MvPolynomial (Fin n) k)) : BR_affine (affineSpaceTriple k (n + m) (I.map (coordInclFst n m)) hI') (CategoryTheory.CategoryStruct.comp emb (coordInclFst n m)) = BR_affine (affineSpaceTriple k n I hI) emb

Stabilisation along 𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ does not change BR_affine [Kol07, Theorem 36, proof], granted the identity of [Kol07, Theorem 35 (5)] for the two principalization sequences.

instance Hironaka.Resolution.isClosedImmersion_coordInclSnd_affineSpaceTriple {k : Type u} [Field k] {n m : ℕ} (I : (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin m) k)).IdealSheafData) (hI : I.IsNonzeroEverywhere) (hI' : (I.map (coordInclSnd n m)).IsNonzeroEverywhere) : AlgebraicGeometry.IsClosedImmersion (coordInclSnd n m)

The second coordinate inclusion, typed at the triples' ambients, is a closed immersion.

instance Hironaka.Resolution.isClosedImmersion_coordInclSnd_affineSpaceTriple' {k : Type u} [Field k] {n m : ℕ} (I : (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin m) k)).IdealSheafData) (hI : I.IsNonzeroEverywhere) : AlgebraicGeometry.IsClosedImmersion (coordInclSnd n m)

The same instance with the target read as the affine space itself.

theorem Hironaka.Resolution.affineSpaceTriple_closedEmbedding_coordInclSnd {k : Type u} [Field k] {n m : ℕ} (I : (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin m) k)).IdealSheafData) (hI : I.IsNonzeroEverywhere) (hI' : (I.map (coordInclSnd n m)).IsNonzeroEverywhere) : (affineSpaceTriple k (n + m) (I.map (coordInclSnd n m)) hI').ClosedEmbedding (affineSpaceTriple k m I hI) (coordInclSnd n m)

The second coordinate inclusion 𝔸ᵐ ↪ 𝔸ⁿ⁺ᵐ is a closed embedding of triples (𝔸ᵐ, I, ∅) ↪ (𝔸ⁿ⁺ᵐ, I.map (coordInclSnd n m), ∅), the situation of [Kol07, Theorem 35 (5)].