Zariski Cancellation

Reference: arxiv/2208.14736 The Zariski Cancellation Problem and related problems in Affine Algebraic Geometry by Neena Gupta

def Arxiv.«2208.14736».IsCancellative (k : Type u_1) (A : Type u_2) [Field k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] : Prop

A finitely generated k-algebra A is cancellative if for all finitely generated k algebras B such that B[X] ≅ₖ A[X] we have B ≅ₖ A.

Equations

• Arxiv.«2208.14736».IsCancellative k A = ∀ {B : Type ?u.36} [inst : CommRing B] [inst_1 : Algebra k B] [Algebra.FiniteType k B], Nonempty (Polynomial A ≃ₐ[k] Polynomial B) → Nonempty (A ≃ₐ[k] B)

theorem Arxiv.«2208.14736».zariski_cancellation_problem {k : Type u_1} [Field k] [CharZero k] {ι : Type u_2} [Fintype ι] : IsCancellative k (MvPolynomial ι k)

The Zariski Cancellation Problem: every polynomial ring over a field k of characteristic 0 is cancellative.

theorem Arxiv.«2208.14736».zariski_cancellation_problem.variants.dim_one {k : Type u_1} [Field k] : IsCancellative k (Polynomial k)

The single variable polynomial ring k[X] is cancellative in any characteristic

theorem Arxiv.«2208.14736».zariski_cancellation_problem.variants.dim_two {k : Type u_1} [Field k] : IsCancellative k (MvPolynomial (Fin 2) k)

The two variable polynomial ring k[X] is cancellative in any characteristic

theorem Arxiv.«2208.14736».zariski_cancellation_problem.variants.false_pos_card (p : ℕ) [hp : Fact (Nat.Prime p)] {ι : Type u_1} [Fintype ι] (hι : Fintype.card ι = 3) : ¬IsCancellative (ZMod p) (MvPolynomial ι (ZMod p))

The positive characteristic case of the Zariski Cancellation Problem is false in dimension 3