Chart transitions of the affine blow-up algebras #
For a, b ∈ I the localizations R[I/a]_{b/a} and R[I/b]_{a/b} are canonically isomorphic
R-algebras: both are the subring of R_{ab} generated by I/a, I/b, a/b, b/a. This is
the gluing of the charts of the blow-up along the inclusions R_{gⱼ}, R_{gₗ} ⊆ R_{gⱼgₗ}
[Hau14, Definition 4.13], the identity D₊(f) ∩ D₊(g) = D₊(fg) for Proj.
Main declarations #
AlgebraicGeometry.awayToAwayₐ x c h : Localization.Away x →ₐ[R] Localization.Away cforx ∣ c.affineBlowUpAlgebra.toAway I hac : R[I/a] →ₐ[R] Localization.Away cfora ∣ c.affineBlowUpAlgebra.embed I hac s hs : Localization.Away s →ₐ[R] Localization.Away cfor an elementsofR[I/a]whose image inR_cis a unit;embed_injectivewhenc = s · aᵐinR[I/a].affineBlowUpAlgebra.transitionEquiv I ha hb : R[I/a]_{b/a} ≃ₐ[R] R[I/b]_{a/b}withtransitionEquiv_spec,transitionEquiv_unique, andembedAB_injective,range_embedAB_eqfor the "subring ofR_{ab}" statement.
The argument #
The unlocalized map R[I/a] → R_{ab} need not be injective when b is a zero divisor, so all
identities are proved after localizing at b/a. The map R[I/a]_{b/a} → R_{ab} is injective:
if w/(b/a)ᵐ ↦ 0 then w ↦ 0 in R_{ab}; writing w = r/aⁿ in R_a, (ab)ᵏ r = 0 in R, so
bᵏ w = 0 in R_a, hence in R[I/a]; since b = (b/a)·a with b/a a unit of the localization
and a a nonzerodivisor of R[I/a] (affineBlowUpAlgebra.algebraMap_mem_nonZeroDivisors),
w = 0 there. The two images coincide: each is the R-subalgebra of R_{ab} generated by the
x/a, the x/b and a/b, b/a (the inverse of b/a is a/b, an element of the other chart).
The transition is the composite of the two embeddings through their common image. Uniqueness:
an R-algebra map out of R[I/a]_{b/a} is determined by its values on R[I/a], hence on the
generators x/a, and the value at x/a is pinned by e(x/a)·(a/b) = x/b since a/b is a unit.
Conventions #
The target R_c is kept general (a ∣ c): c = ab for the pairwise transition and c = abc'
for the triple one, so that both sides of a transition land in the same ring. Fractions are
handled through multiplicative identities in R_c, never through inverses.
Boundary cases #
b = a: the transition is the identity of R[I/a]_{1} up to the identification 1 = a/a.
Zero divisors among a, b are allowed. If ab = 0 then R_{ab} = 0 and both localizations
are the zero ring, consistently.
The map R_x → R_c for x ∣ c, as an R-algebra map.
Equations
Instances For
The natural map R[I/a] ⊆ R_a → R_c for a ∣ c.
Equations
Instances For
The embedding R[I/a]_s → R_c extending R[I/a] → R_c, for s with unit image.
Equations
Instances For
R[I/a]_s → R_c is injective when c = s · aᵐ in R[I/a]: an element w/sᵐ mapping to zero
has w ↦ 0 in R_c, so cᵏ w = 0 in R[I/a]; s is a unit of the localization and a a
nonzerodivisor, so w = 0 there.
A subalgebra of R_c containing the images of the x/a and an inverse of the image of s
contains the image of R[I/a]_s.
The embedding R[I/a]_{b/a} → R_{ab}.
Equations
Instances For
The embedding R[I/b]_{a/b} → R_{ab}.
Equations
Instances For
R[I/a]_{b/a} → R_{ab} is injective: R[I/a]_{b/a} is a subring of R_{ab}.
The transition isomorphism R[I/a]_{b/a} ≃ R[I/b]_{a/b} [Hau14, Definition 4.13]: the
composite of the two embeddings into R_{ab} through their common image.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The transition sends x/a to (x/b)·(a/b)⁻¹, i.e. e(x/a) · (a/b) = x/b.
The transition is the unique R-algebra isomorphism with e(x/a) · (a/b) = x/b for all
x ∈ I.