Affinoid algebras

An affinoid algebra is a quotient of a Tate algebra in finitely many variables. The predicate TauCeti.IsAffinoidAlgebra is algebraic: it chooses neither a norm nor a topology. In particular, it includes nonreduced algebras and the zero algebra. The native restricted-series subring at unit polyradius is used throughout.

def TauCeti.IsAffinoidAlgebra (K : Type u_1) [NormedField K] [IsUltrametricDist K] (A : Type u_2) [CommRing A] [Algebra K A] : Prop

An affinoid algebra is a quotient of a finite-variable Tate algebra, without a choice of norm or topology on the quotient.

theorem TauCeti.isAffinoidAlgebra_iff (K : Type u_1) [NormedField K] [IsUltrametricDist K] (A : Type u_2) [CommRing A] [Algebra K A] : IsAffinoidAlgebra K A ↔ ∃ (n : ℕ) (π : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1) →ₐ[K] A), Function.Surjective ⇑π

The presentation criterion for an affinoid algebra.

theorem TauCeti.isAffinoidAlgebra_tate {K : Type u_1} [NormedField K] [IsUltrametricDist K] {σ : Type u_3} [Finite σ] : IsAffinoidAlgebra K ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1)

A Tate algebra in finitely many variables is affinoid.

theorem TauCeti.isAffinoidAlgebra_self {K : Type u_1} [NormedField K] [IsUltrametricDist K] : IsAffinoidAlgebra K K

The coefficient field is affinoid, using the Tate presentation in zero variables.

theorem TauCeti.IsAffinoidAlgebra.of_surjective {K : Type u_1} [NormedField K] [IsUltrametricDist K] {A : Type u_2} [CommRing A] [Algebra K A] (hA : IsAffinoidAlgebra K A) {B : Type u_3} [CommRing B] [Algebra K B] (f : A →ₐ[K] B) (hf : Function.Surjective ⇑f) : IsAffinoidAlgebra K B

A surjective image of an affinoid algebra is affinoid.

theorem TauCeti.IsAffinoidAlgebra.quotient {K : Type u_1} [NormedField K] [IsUltrametricDist K] {A : Type u_2} [CommRing A] [Algebra K A] (hA : IsAffinoidAlgebra K A) (I : Ideal A) : IsAffinoidAlgebra K (A ⧸ I)

Every quotient of an affinoid algebra is affinoid, including the zero quotient.