Affine blowup algebras

Let A be a commutative semiring, I an ideal of A and a ∈ A. The affine blowup algebra A[I/a] is the A-subalgebra of the localization A_a generated by the fractions i/a for i ∈ I. When a ∈ I, its elements are exactly the fractions y/aᵏ with y ∈ Iᵏ, and for a ring A it is the ring of the affine chart D₊(a) of the blowup of Spec A along I.

The two basic properties of A[I/a] are that, when a ∈ I, the extension of I to it is the principal ideal generated by a, and that multiplication by a is injective in it. It is universal with these properties: if B is a commutative A-semialgebra such that I B ⊆ a B and multiplication by a is injective in B, then there is a unique A-algebra map A[I/a] → B. For rings, injectivity is equivalent to a being a nonzerodivisor. The blowup of a scheme along a closed subscheme is glued from these affine charts.

Main definitions

• Ideal.affineBlowup I a S: the affine blowup algebra A[I/a], as a subalgebra of a localization S of A away from a.
• Ideal.affineBlowupLift: the A-algebra map A[I/a] → B of the universal property.

Main results

• Ideal.affineBlowup_eq_adjoin_of_span_eq: if I is generated by s, then A[I/a] is generated by the fractions x/a for x ∈ s.
• Ideal.mem_affineBlowup_iff: for a ∈ I, the elements of A[I/a] are the fractions y/aᵏ with y ∈ Iᵏ.
• Ideal.map_algebraMap_affineBlowup: for a ∈ I, the ideal I A[I/a] is generated by a.
• Ideal.isRegular_algebraMap_affineBlowup: multiplication by a is injective in A[I/a].
• Ideal.algebraMap_mul_algHom_divBy: an A-algebra map out of A[I/a] sends i/a to an element whose product with a is i.
• Ideal.affineBlowup_algHom_ext: uniqueness in the universal property of A[I/a].

References

• The Stacks Project, Section Blow up algebras

noncomputable def Ideal.affineBlowup {A : Type u_1} [CommSemiring A] (I : Ideal A) (a : A) (S : Type u_2) [CommSemiring S] [Algebra A S] [IsLocalization.Away a S] : Subalgebra A S

The affine blowup algebra A[I/a]: the A-subalgebra of a localization S of A away from a generated by the fractions i/a with i ∈ I. When a ∈ I it is the coordinate ring of the chart D₊(a) of the blowup of Spec A along I.

Equations

• I.affineBlowup a S = Algebra.adjoin A ((fun (i : A) => TauCeti.Localization.divBy i a) '' ↑I)

theorem Ideal.affineBlowup_def {A : Type u_1} [CommSemiring A] (I : Ideal A) (a : A) (S : Type u_2) [CommSemiring S] [Algebra A S] [IsLocalization.Away a S] : I.affineBlowup a S = Algebra.adjoin A ((fun (i : A) => TauCeti.Localization.divBy i a) '' ↑I)

A[I/a] is generated over A by the fractions i/a with i ∈ I.

theorem Ideal.divBy_mem_affineBlowup {A : Type u_1} [CommSemiring A] {I : Ideal A} {a : A} {S : Type u_2} [CommSemiring S] [Algebra A S] [IsLocalization.Away a S] {i : A} (hi : i ∈ I) : TauCeti.Localization.divBy i a ∈ I.affineBlowup a S

The fraction i/a lies in A[I/a] for every i ∈ I.

theorem Ideal.affineBlowup_le_iff {A : Type u_1} [CommSemiring A] {I : Ideal A} {a : A} {S : Type u_2} [CommSemiring S] [Algebra A S] [IsLocalization.Away a S] {B : Subalgebra A S} : I.affineBlowup a S ≤ B ↔ ∀ i ∈ I, TauCeti.Localization.divBy i a ∈ B

A subalgebra of S contains A[I/a] exactly when it contains every fraction i/a with i ∈ I.

theorem Ideal.affineBlowup_eq_adjoin_of_span_eq {A : Type u_1} [CommSemiring A] {I : Ideal A} {a : A} {S : Type u_2} [CommSemiring S] [Algebra A S] [IsLocalization.Away a S] {s : Set A} (hs : span s = I) : I.affineBlowup a S = Algebra.adjoin A ((fun (x : A) => TauCeti.Localization.divBy x a) '' s)

Generators of A[I/a]. If the ideal I is generated by s, then A[I/a] is generated over A by the fractions x/a with x ∈ s.

theorem Ideal.mem_affineBlowup_iff {A : Type u_1} [CommSemiring A] {I : Ideal A} {a : A} {S : Type u_2} [CommSemiring S] [Algebra A S] [IsLocalization.Away a S] (ha : a ∈ I) {z : S} : z ∈ I.affineBlowup a S ↔ ∃ (k : ℕ), ∃ y ∈ I ^ k, (algebraMap A S) a ^ k * z = (algebraMap A S) y

The elements of A[I/a]. For a ∈ I, an element z of the localization S lies in A[I/a] exactly when aᵏ z ∈ Iᵏ for some k, that is, when z is a fraction y/aᵏ with y ∈ Iᵏ.

theorem Ideal.map_algebraMap_affineBlowup {A : Type u_1} [CommSemiring A] {I : Ideal A} {a : A} {S : Type u_2} [CommSemiring S] [Algebra A S] [IsLocalization.Away a S] (ha : a ∈ I) : map (algebraMap A ↥(I.affineBlowup a S)) I = span {(algebraMap A ↥(I.affineBlowup a S)) a}

The exceptional ideal is principal. For a ∈ I, the extension of I to A[I/a] is the principal ideal generated by a.

theorem Ideal.isRegular_algebraMap_affineBlowup {A : Type u_1} [CommSemiring A] {I : Ideal A} {a : A} {S : Type u_2} [CommSemiring S] [Algebra A S] [IsLocalization.Away a S] : IsRegular ((algebraMap A ↥(I.affineBlowup a S)) a)

Multiplication by a is injective in A[I/a].

theorem Ideal.algebraMap_mul_algHom_divBy {A : Type u_1} [CommSemiring A] {I : Ideal A} {a : A} {S : Type u_2} [CommSemiring S] [Algebra A S] [IsLocalization.Away a S] {B : Type u_3} [Semiring B] [Algebra A B] (f : ↥(I.affineBlowup a S) →ₐ[A] B) {i : A} (hi : i ∈ I) : (algebraMap A B) a * f ⟨TauCeti.Localization.divBy i a, ⋯⟩ = (algebraMap A B) i

An A-algebra map out of A[I/a] sends i/a to an element whose product with a is i.

theorem Ideal.affineBlowup_algHom_ext {A : Type u_1} [CommSemiring A] {I : Ideal A} {a : A} {S : Type u_2} [CommSemiring S] [Algebra A S] [IsLocalization.Away a S] {B : Type u_3} [Semiring B] [Algebra A B] (ha : IsLeftRegular ((algebraMap A B) a)) {f g : ↥(I.affineBlowup a S) →ₐ[A] B} : f = g

Uniqueness in the universal property of A[I/a]. Two A-algebra maps from A[I/a] to an A-semialgebra in which left multiplication by a is injective are equal.

theorem Ideal.instAwayCoeAlgHomOfIdAwayRingHomAlgebraMap_tauCeti {A : Type u_1} [CommSemiring A] {a : A} {B : Type u_3} [CommSemiring B] [Algebra A B] : IsLocalization.Away ((Algebra.ofId A B) a) (Localization.Away ((algebraMap A B) a))

noncomputable def Ideal.affineBlowupLift {A : Type u_1} [CommSemiring A] (I : Ideal A) (a : A) (S : Type u_2) [CommSemiring S] [Algebra A S] [IsLocalization.Away a S] {B : Type u_3} [CommSemiring B] [Algebra A B] (hI : map (algebraMap A B) I ≤ span {(algebraMap A B) a}) (ha : IsLeftRegular ((algebraMap A B) a)) : ↥(I.affineBlowup a S) →ₐ[A] B

The universal property of A[I/a]. If B is a commutative A-semialgebra with I B ⊆ a B and multiplication by a injective in B, this is the A-algebra map A[I/a] → B. For rings, the injectivity hypothesis is equivalent to a being a nonzerodivisor by isLeftRegular_iff_mem_nonZeroDivisorsLeft. It sends i/a to the element b ∈ B with a b = i (Ideal.algebraMap_mul_algHom_divBy), and it is the only A-algebra map A[I/a] → B (Ideal.affineBlowup_algHom_ext).

Equations

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