The shears of affine space are automorphisms

The proof of [Kol07, Lemma 39] uses that (x, y) ↦ (x, y + j₂(x)) and (x, y) ↦ (x + j₁(y), y) are automorphisms of 𝔸ⁿ⁺ᵐ. This file proves it for the shears shearY v and shearX w of Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineSpace: composition of polynomial maps is substitution (polynomialMap_comp), the polynomial map of the coordinates is the identity (polynomialMap_X), and the substitutions of v and -v cancel on the generators, so shearY (-v) is the inverse of shearY v (shearY_comp_shearY_neg, isIso_shearY), and likewise for shearX.

The IsIso instances are used in the proof of Lemma 39 (exists_aut_conj_embeddings in Hironaka.Resolution.Algebraic.Kol07.Thm36.Lemma39), where the conjugating automorphism is shearY v ≫ inv (shearX w).

Composition and identity of polynomial maps

theorem Hironaka.Resolution.polynomialMap_comp {k : Type u} [Field k] {n m p : ℕ} (v : Fin m → MvPolynomial (Fin n) k) (w : Fin p → MvPolynomial (Fin m) k) : CategoryTheory.CategoryStruct.comp (polynomialMap v) (polynomialMap w) = polynomialMap fun (j : Fin p) => (MvPolynomial.aeval v) (w j)

Composition of polynomial maps is substitution: polynomialMap v ≫ polynomialMap w is the polynomial map with components aeval v (w j).

theorem Hironaka.Resolution.polynomialMap_X {k : Type u} [Field k] {n : ℕ} : (polynomialMap fun (i : Fin n) => MvPolynomial.X i) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin n) k))

The polynomial map of the coordinates is the identity.

theorem Hironaka.Resolution.polynomialMap_congr {k : Type u} [Field k] {n m : ℕ} {v w : Fin m → MvPolynomial (Fin n) k} (h : ∀ (j : Fin m), v j = w j) : polynomialMap v = polynomialMap w

Two polynomial maps with the same components are equal (componentwise extensionality).

The inverses of the shears

theorem Hironaka.Resolution.aeval_shearYFun_rename {k : Type u} [Field k] {n m : ℕ} (v : Fin m → MvPolynomial (Fin n) k) (p : MvPolynomial (Fin n) k) : (MvPolynomial.aeval fun (j : Fin (n + m)) => Sum.elim (coordX n m) (fun (l : Fin m) => coordY n m l + (MvPolynomial.rename fun (i : Fin n) => finSumFinEquiv (Sum.inl i)) (v l)) (finSumFinEquiv.symm j)) ((MvPolynomial.rename fun (i : Fin n) => finSumFinEquiv (Sum.inl i)) p) = (MvPolynomial.rename fun (i : Fin n) => finSumFinEquiv (Sum.inl i)) p

Substituting the coordinates of the first block into a polynomial renamed into the first block gives it back: aeval (shearY v's components) (rename inl p) = rename inl p.

theorem Hironaka.Resolution.aeval_shearXFun_rename {k : Type u} [Field k] {n m : ℕ} (w : Fin n → MvPolynomial (Fin m) k) (p : MvPolynomial (Fin m) k) : (MvPolynomial.aeval fun (j : Fin (n + m)) => Sum.elim (fun (i : Fin n) => coordX n m i + (MvPolynomial.rename fun (l : Fin m) => finSumFinEquiv (Sum.inr l)) (w i)) (coordY n m) (finSumFinEquiv.symm j)) ((MvPolynomial.rename fun (l : Fin m) => finSumFinEquiv (Sum.inr l)) p) = (MvPolynomial.rename fun (l : Fin m) => finSumFinEquiv (Sum.inr l)) p

Substituting the coordinates of the second block into a polynomial renamed into the second block gives it back.

theorem Hironaka.Resolution.shearY_comp_shearY_neg {k : Type u} [Field k] {n m : ℕ} (v : Fin m → MvPolynomial (Fin n) k) : CategoryTheory.CategoryStruct.comp (shearY v) (shearY (-v)) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin (n + m)) k))

The shear shearY v followed by shearY (-v) is the identity; so the automorphism (x, y) ↦ (x, y + j₂(x)) of the proof of [Kol07, Lemma 39] is inverted by y ↦ y − j₂(x).

theorem Hironaka.Resolution.shearX_comp_shearX_neg {k : Type u} [Field k] {n m : ℕ} (w : Fin n → MvPolynomial (Fin m) k) : CategoryTheory.CategoryStruct.comp (shearX w) (shearX (-w)) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin (n + m)) k))

The shear shearX w followed by shearX (-w) is the identity; so the automorphism (x, y) ↦ (x + j₁(y), y) of the proof of [Kol07, Lemma 39] is inverted by x ↦ x − j₁(y).

instance Hironaka.Resolution.isIso_shearY {k : Type u} [Field k] {n m : ℕ} (v : Fin m → MvPolynomial (Fin n) k) : CategoryTheory.IsIso (shearY v)

shearY v is an automorphism of 𝔸ⁿ⁺ᵐ [Kol07, Lemma 39, proof].

instance Hironaka.Resolution.isIso_shearX {k : Type u} [Field k] {n m : ℕ} (w : Fin n → MvPolynomial (Fin m) k) : CategoryTheory.IsIso (shearX w)

shearX w is an automorphism of 𝔸ⁿ⁺ᵐ [Kol07, Lemma 39, proof].