The exceptional divisor of the model blow-up in a chart

The exceptional divisor E = π⁻¹(Z) [Hau14, Definition 4.7], a hypersurface [Hau14, Example 5.9], computed in the chart U_j: the exceptional ideal I·𝒪_B pulls back along U_j to the ideal sheaf of (x_j) — on the chart of x_j the exceptional ideal is (x_j) in A[x][L/x_j] (affineBlowUp.comap_exceptionalIdeal_chart), and x_j ↦ x_j under the identification with A[x]. The quotient A[x]/(x_j) is the polynomial ring over A in the remaining variables, through Mathlib's killCompl (kill the variable x_j), whose kernel is (x_j): a polynomial is congruent modulo (x_j) to the renaming of its image, because a monomial either avoids x_j (and is recovered from its image) or is divisible by x_j. Hence F ∩ U_j ≅ 𝔸^{n-1}_A, smooth of relative dimension n - 1 (the standard smoothness of polynomial rings, Hironaka.Scheme.BlowUp.CoordinateSubspace.Smooth), and through the chart map π_j it is the affine space 𝔸^{r-1}_L over the centre. The quotient identifications are used for the exceptional divisor of blow-ups of smooth centres (Hironaka.Scheme.Smooth.ExceptionalModel) and in the worked examples (HironakaExamples.Sequence.Remark33Charts, HironakaExamples.OrderReduction.Example106BlowUp).

theorem AlgebraicGeometry.CoordinateSubspace.comap_exceptionalIdeal_modelChart (A : Type u) [CommRing A] (n r : ℕ) (j : Fin n) (hj : ↑j < r) : (affineBlowUp.exceptionalIdeal (centerIdeal A n r)).comap (modelChart A n r j hj) = Scheme.IdealSheafData.ofIdealTop (Ideal.map (CommRingCat.Hom.hom (Scheme.ΓSpecIso ↧(MvPolynomial (Fin n) A)).inv) (Ideal.span {MvPolynomial.X j}))

In the chart U_j the exceptional divisor is V(x_j) [Hau14, Definition 4.7].

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.CoordinateSubspace.killPred (A : Type u) [CommRing A] {n : ℕ} (p : Fin n → Prop) : MvPolynomial (Fin n) A →ₐ[A] MvPolynomial { i : Fin n // p i } A

Killing the variables x_i with ¬ p i: the A-algebra map A[x_0, …, x_{n-1}] → A[x_i : p i] (Mathlib's killCompl for the inclusion of the subtype).

Equations

• AlgebraicGeometry.CoordinateSubspace.killPred A p = MvPolynomial.killCompl ⋯

theorem AlgebraicGeometry.CoordinateSubspace.killPred_X_of (A : Type u) [CommRing A] {n : ℕ} (p : Fin n → Prop) {i : Fin n} (h : p i) : (killPred A p) (MvPolynomial.X i) = MvPolynomial.X ⟨i, h⟩

theorem AlgebraicGeometry.CoordinateSubspace.killPred_X_of_not (A : Type u) [CommRing A] {n : ℕ} (p : Fin n → Prop) {i : Fin n} (h : ¬p i) : (killPred A p) (MvPolynomial.X i) = 0

theorem AlgebraicGeometry.CoordinateSubspace.killPred_surjective (A : Type u) [CommRing A] {n : ℕ} (p : Fin n → Prop) : Function.Surjective ⇑(killPred A p)

theorem AlgebraicGeometry.CoordinateSubspace.sub_rename_killPred_mem (A : Type u) [CommRing A] {n : ℕ} (p : Fin n → Prop) (q : MvPolynomial (Fin n) A) : q - (MvPolynomial.rename Subtype.val) ((killPred A p) q) ∈ affineBlowUpAlgebra.coordinateIdeal A {i : Fin n | ¬p i}

A polynomial is congruent modulo (x_i : ¬ p i) to the renaming of its image under killPred.

theorem AlgebraicGeometry.CoordinateSubspace.ker_killPred (A : Type u) [CommRing A] {n : ℕ} (p : Fin n → Prop) : RingHom.ker ↑(killPred A p) = affineBlowUpAlgebra.coordinateIdeal A {i : Fin n | ¬p i}

noncomputable def AlgebraicGeometry.CoordinateSubspace.quotientCoordinateIdealAlgEquiv (A : Type u) [CommRing A] {n : ℕ} (p : Fin n → Prop) : (MvPolynomial (Fin n) A ⧸ affineBlowUpAlgebra.coordinateIdeal A {i : Fin n | ¬p i}) ≃ₐ[A] MvPolynomial { i : Fin n // p i } A

A[x]/(x_i : ¬ p i) ≃ A[x_i : p i], x_i ↦ x_i.

Equations

• AlgebraicGeometry.CoordinateSubspace.quotientCoordinateIdealAlgEquiv A p = (Ideal.quotientEquivAlgOfEq A ⋯).trans (Ideal.quotientKerAlgEquivOfSurjective ⋯)

theorem AlgebraicGeometry.CoordinateSubspace.quotientCoordinateIdealAlgEquiv_mk_X (A : Type u) [CommRing A] {n : ℕ} (p : Fin n → Prop) {i : Fin n} (h : p i) : (quotientCoordinateIdealAlgEquiv A p) ((Ideal.Quotient.mk (affineBlowUpAlgebra.coordinateIdeal A {i : Fin n | ¬p i})) (MvPolynomial.X i)) = MvPolynomial.X ⟨i, h⟩

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.CoordinateSubspace.killX (A : Type u) [CommRing A] {n : ℕ} (j : Fin n) : MvPolynomial (Fin n) A →ₐ[A] MvPolynomial { i : Fin n // i ≠ j } A

Killing the variable x_j: the A-algebra map A[x_0, …, x_{n-1}] → A[x_i : i ≠ j].

Equations

• AlgebraicGeometry.CoordinateSubspace.killX A j = AlgebraicGeometry.CoordinateSubspace.killPred A fun (x : Fin n) => x ≠ j

theorem AlgebraicGeometry.CoordinateSubspace.killX_X_of_ne (A : Type u) [CommRing A] {n : ℕ} (j : Fin n) {i : Fin n} (h : i ≠ j) : (killX A j) (MvPolynomial.X i) = MvPolynomial.X ⟨i, h⟩

theorem AlgebraicGeometry.CoordinateSubspace.killX_X_self (A : Type u) [CommRing A] {n : ℕ} (j : Fin n) : (killX A j) (MvPolynomial.X j) = 0

theorem AlgebraicGeometry.CoordinateSubspace.killX_surjective (A : Type u) [CommRing A] {n : ℕ} (j : Fin n) : Function.Surjective ⇑(killX A j)

theorem AlgebraicGeometry.CoordinateSubspace.ker_killX (A : Type u) [CommRing A] {n : ℕ} (j : Fin n) : RingHom.ker ↑(killX A j) = Ideal.span {MvPolynomial.X j}

noncomputable def AlgebraicGeometry.CoordinateSubspace.quotientSpanXAlgEquiv (A : Type u) [CommRing A] {n : ℕ} (j : Fin n) : (MvPolynomial (Fin n) A ⧸ Ideal.span {MvPolynomial.X j}) ≃ₐ[A] MvPolynomial { i : Fin n // i ≠ j } A

A[x]/(x_j) ≃ A[x_i : i ≠ j], x_i ↦ x_i.

Equations

• AlgebraicGeometry.CoordinateSubspace.quotientSpanXAlgEquiv A j = (Ideal.quotientEquivAlgOfEq A ⋯).trans (Ideal.quotientKerAlgEquivOfSurjective ⋯)

theorem AlgebraicGeometry.CoordinateSubspace.quotientSpanXAlgEquiv_mk_X (A : Type u) [CommRing A] {n : ℕ} (j : Fin n) {i : Fin n} (h : i ≠ j) : (quotientSpanXAlgEquiv A j) ((Ideal.Quotient.mk (Ideal.span {MvPolynomial.X j})) (MvPolynomial.X i)) = MvPolynomial.X ⟨i, h⟩

theorem AlgebraicGeometry.CoordinateSubspace.exists_algEquiv_quotient_span_X (A : Type u) [CommRing A] {n : ℕ} (j : Fin n) : ∃ (e : (MvPolynomial (Fin n) A ⧸ Ideal.span {MvPolynomial.X j}) ≃ₐ[A] MvPolynomial { i : Fin n // i ≠ j } A), ∀ (i : Fin n) (h : i ≠ j), e ((Ideal.Quotient.mk (Ideal.span {MvPolynomial.X j})) (MvPolynomial.X i)) = MvPolynomial.X ⟨i, h⟩

theorem AlgebraicGeometry.CoordinateSubspace.card_ne {n : ℕ} (j : Fin n) : Nat.card { i : Fin n // i ≠ j } = n - 1

theorem AlgebraicGeometry.CoordinateSubspace.smoothOfRelativeDimension_quotient_span_X (A : Type u) [CommRing A] {n : ℕ} (j : Fin n) : SmoothOfRelativeDimension (n - 1) (Spec.map (CommRingCat.ofHom (algebraMap A (MvPolynomial (Fin n) A ⧸ Ideal.span {MvPolynomial.X j}))))

F ∩ U_j ≅ 𝔸^{n-1}_A is smooth over A of relative dimension n - 1.

theorem AlgebraicGeometry.CoordinateSubspace.centerIdeal_eq_coordinateIdeal_not_not (A : Type u) [CommRing A] (n r : ℕ) : centerIdeal A n r = affineBlowUpAlgebra.coordinateIdeal A {i : Fin n | ¬¬↑i < r}

noncomputable def AlgebraicGeometry.CoordinateSubspace.quotientCenterAlgEquiv (A : Type u) [CommRing A] (n r : ℕ) : (MvPolynomial (Fin n) A ⧸ centerIdeal A n r) ≃ₐ[A] MvPolynomial { i : Fin n // ¬↑i < r } A

A[x]/I ≃ A[x_i : r ≤ i]: the coordinate subspace L is 𝔸^{n-r}_A.

Equations

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

theorem AlgebraicGeometry.CoordinateSubspace.quotientCenterAlgEquiv_mk_X (A : Type u) [CommRing A] (n r : ℕ) {i : Fin n} (h : ¬↑i < r) : (quotientCenterAlgEquiv A n r) ((Ideal.Quotient.mk (centerIdeal A n r)) (MvPolynomial.X i)) = MvPolynomial.X ⟨i, h⟩

def AlgebraicGeometry.CoordinateSubspace.splitVars (n r : ℕ) (j : Fin n) (hj : ↑j < r) : { i : Fin n // ↑i < r ∧ i ≠ j } ⊕ { i : Fin n // ¬↑i < r } ≃ { i : Fin n // i ≠ j }

The variables x_i, i ≠ j, split into the fibre directions i < r and the directions r ≤ i of the base L.

Equations

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

theorem AlgebraicGeometry.CoordinateSubspace.splitVars_symm_of_lt (n r : ℕ) (j : Fin n) (hj : ↑j < r) {i : Fin n} (hij : i ≠ j) (h : ↑i < r) : (splitVars n r j hj).symm ⟨i, hij⟩ = Sum.inl ⟨i, ⋯⟩

theorem AlgebraicGeometry.CoordinateSubspace.splitVars_symm_of_not_lt (n r : ℕ) (j : Fin n) (hj : ↑j < r) {i : Fin n} (hij : i ≠ j) (h : ¬↑i < r) : (splitVars n r j hj).symm ⟨i, hij⟩ = Sum.inr ⟨i, h⟩

noncomputable def AlgebraicGeometry.CoordinateSubspace.fibreAlgEquiv (A : Type u) [CommRing A] (n r : ℕ) (j : Fin n) (hj : ↑j < r) : (MvPolynomial (Fin n) A ⧸ Ideal.span {MvPolynomial.X j}) ≃ₐ[A] MvPolynomial { i : Fin n // ↑i < r ∧ i ≠ j } (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)

A[x]/(x_j) ≃ (A[x]/I)[x_i : i < r, i ≠ j] as A-algebras.

Equations

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

theorem AlgebraicGeometry.CoordinateSubspace.fibreAlgEquiv_mk_X_of (A : Type u) [CommRing A] (n r : ℕ) (j : Fin n) (hj : ↑j < r) {i : Fin n} (h : ↑i < r ∧ i ≠ j) : (fibreAlgEquiv A n r j hj) ((Ideal.Quotient.mk (Ideal.span {MvPolynomial.X j})) (MvPolynomial.X i)) = MvPolynomial.X ⟨i, h⟩

theorem AlgebraicGeometry.CoordinateSubspace.fibreAlgEquiv_mk_X_of_not_lt (A : Type u) [CommRing A] (n r : ℕ) (j : Fin n) (hj : ↑j < r) {i : Fin n} (h : ¬↑i < r) : (fibreAlgEquiv A n r j hj) ((Ideal.Quotient.mk (Ideal.span {MvPolynomial.X j})) (MvPolynomial.X i)) = MvPolynomial.C ((Ideal.Quotient.mk (centerIdeal A n r)) (MvPolynomial.X i))

theorem AlgebraicGeometry.CoordinateSubspace.fibreAlgEquiv_comp_mk_comp_chartSubst (A : Type u) [CommRing A] (n r : ℕ) (j : Fin n) (hj : ↑j < r) : (↑(fibreAlgEquiv A n r j hj)).comp ((Ideal.Quotient.mkₐ A (Ideal.span {MvPolynomial.X j})).comp (affineBlowUpAlgebra.chartSubst A (center n r) j)) = (IsScalarTower.toAlgHom A (MvPolynomial (Fin n) A ⧸ centerIdeal A n r) (MvPolynomial { i : Fin n // ↑i < r ∧ i ≠ j } (MvPolynomial (Fin n) A ⧸ centerIdeal A n r))).comp (Ideal.Quotient.mkₐ A (centerIdeal A n r))

The chart map π_j followed by A[x]/(x_j) ≃ (A[x]/I)[x_i : i < r, i ≠ j] is the structure map of the polynomial ring over A[x]/I: it kills x_i for i < r and sends x_i to the constant x_i for r ≤ i.

noncomputable def AlgebraicGeometry.CoordinateSubspace.fibreAlgEquivOverCenter (A : Type u) [CommRing A] (n r : ℕ) (j : Fin n) (hj : ↑j < r) : (MvPolynomial (Fin n) A ⧸ Ideal.span {MvPolynomial.X j}) ≃ₐ[MvPolynomial (Fin n) A ⧸ centerIdeal A n r] MvPolynomial { i : Fin n // ↑i < r ∧ i ≠ j } (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)

A[x]/(x_j) ≃ (A[x]/I)[x_i : i < r, i ≠ j] as algebras over 𝒪(L) = A[x]/I, the structure of A[x]/(x_j) over A[x]/I being through the chart map π_j [Hau14, Example 5.9].

Equations

• AlgebraicGeometry.CoordinateSubspace.fibreAlgEquivOverCenter A n r j hj = AlgEquiv.ofRingEquiv ⋯

theorem AlgebraicGeometry.CoordinateSubspace.exists_algEquiv_quotient_span_X_over_center (A : Type u) [CommRing A] (n r : ℕ) (j : Fin n) (hj : ↑j < r) : ∃ (e : (MvPolynomial (Fin n) A ⧸ Ideal.span {MvPolynomial.X j}) ≃ₐ[MvPolynomial (Fin n) A ⧸ centerIdeal A n r] MvPolynomial { i : Fin n // ↑i < r ∧ i ≠ j } (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)), ∀ (i : Fin n) (h : ↑i < r ∧ i ≠ j), e ((Ideal.Quotient.mk (Ideal.span {MvPolynomial.X j})) (MvPolynomial.X i)) = MvPolynomial.X ⟨i, h⟩

The exceptional divisor in a chart is an affine space over the centre [Hau14, Example 5.9]: through the chart map π_j, A[x]/(x_j) is the polynomial ring over 𝒪(L) = A[x]/I in the r - 1 variables x_i, i < r, i ≠ j.