Teichmüller map

Let R be an I-adically complete ring, and p be a prime number with p ∈ I.

Then there is a canonical map Perfection (R ⧸ I) p →*₀ R that we shall call Perfection.teichmuller, such that it composed with the quotient map R →+* R ⧸ I is the "0-th coefficient" map Perfection (R ⧸ I) p →+* R ⧸ I.

noncomputable def Perfection.teichmullerAux {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] (x : Perfection (R ⧸ I) p) : ℕ → R

An auxiliary sequence to define the Teichmüller map. The (n + 1)-st term is the p^n-th power of an arbitrary lift in R of the n-th component from the perfection of R ⧸ I.

theorem Perfection.teichmullerAux_sModEq {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] (x : Perfection (R ⧸ I) p) (m : ℕ) : x.teichmullerAux m ≡ x.teichmullerAux (m + 1) [SMOD I ^ m]

noncomputable def Perfection.teichmullerCauchy {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] (x : Perfection (R ⧸ I) p) : AdicCompletion.AdicCauchySequence I R

teichmullerAux as an adic Cauchy sequence.

theorem Perfection.exists_teichmullerFun {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsPrecomplete I R] (x : Perfection (R ⧸ I) p) : ∃ (y : R), ∀ (n : ℕ), x.teichmullerAux n ≡ y [SMOD I ^ n • ⊤]

noncomputable def Perfection.teichmullerFun {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsPrecomplete I R] (x : Perfection (R ⧸ I) p) : R

Given an I-adically precomplete ring R, where p ∈ I, this is the underlying function of the Teichmüller map. It is defined as the limit of p^n-th powers of arbitrary lifts in R of the n-th component from the perfection of R ⧸ I.

The simp NF is teichmuller₀ when R is I-adically complete.

theorem Perfection.teichmullerFun_sModEq {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsPrecomplete I R] {x : Perfection (R ⧸ I) p} {y : R} {n : ℕ} (h : (Ideal.Quotient.mk I) y = (coeff (R ⧸ I) p n) x) : x.teichmullerFun ≡ y ^ p ^ n [SMOD I ^ (n + 1)]

theorem Perfection.teichmullerFun_spec' {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R} (h : ∃ (N : ℕ), ∀ n ≥ N, ∃ (z : R), (Ideal.Quotient.mk I) z = (coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]) : x.teichmullerFun = y

theorem Perfection.teichmullerFun_spec {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R} (h : ∀ (n : ℕ), ∃ (z : R), (Ideal.Quotient.mk I) z = (coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]) : x.teichmullerFun = y

noncomputable def Perfection.teichmuller (p : ℕ) [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (I : Ideal R) [CharP (R ⧸ I) p] [IsAdicComplete I R] : Perfection (R ⧸ I) p →* R

Given an I-adically complete ring R, and a prime number p with p ∈ I, this is the multiplicative map from Perfection (R ⧸ I) p to R itself. Specifically, it is defined as the limit of p^n-th powers of arbitrary lifts in R of the n-th component from the perfection of R ⧸ I.

The simp NF is teichmuller₀.

theorem Perfection.teichmuller_sModEq {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R} {n : ℕ} (h : (Ideal.Quotient.mk I) y = (coeff (R ⧸ I) p n) x) : (teichmuller p I) x ≡ y ^ p ^ n [SMOD I ^ (n + 1)]

theorem Perfection.teichmuller_spec' {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R} (h : ∃ (N : ℕ), ∀ n ≥ N, ∃ (z : R), (Ideal.Quotient.mk I) z = (coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]) : (teichmuller p I) x = y

theorem Perfection.teichmuller_spec {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R} (h : ∀ (n : ℕ), ∃ (z : R), (Ideal.Quotient.mk I) z = (coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]) : (teichmuller p I) x = y

theorem Perfection.teichmuller_zero {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] : (teichmuller p I) 0 = 0

noncomputable def Perfection.teichmuller₀ (p : ℕ) [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (I : Ideal R) [CharP (R ⧸ I) p] [IsAdicComplete I R] : Perfection (R ⧸ I) p →*₀ R

teichmuller as a MonoidWithZeroHom. This is the simp NF.

@[simp]

theorem Perfection.teichmuller_eq_teichmuller₀_toMonoidHom {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] : teichmuller p I = ↑(teichmuller₀ p I)

@[simp]

theorem Perfection.coe_teichmuller_eq_teichmuller₀ {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] : ⇑(teichmuller p I) = ⇑(teichmuller₀ p I)

@[simp]

theorem Perfection.teichmullerFun_eq_teichmuller₀ {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] : teichmullerFun = ⇑(teichmuller₀ p I)

theorem Perfection.teichmuller₀_sModEq {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R} {n : ℕ} (h : (Ideal.Quotient.mk I) y = (coeff (R ⧸ I) p n) x) : (teichmuller₀ p I) x ≡ y ^ p ^ n [SMOD I ^ (n + 1)]

theorem Perfection.teichmuller₀_spec' {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R} (h : ∃ (N : ℕ), ∀ n ≥ N, ∃ (z : R), (Ideal.Quotient.mk I) z = (coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]) : (teichmuller₀ p I) x = y

theorem Perfection.teichmuller₀_spec {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R} (h : ∀ (n : ℕ), ∃ (z : R), (Ideal.Quotient.mk I) z = (coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]) : (teichmuller₀ p I) x = y

@[simp]

theorem Perfection.teichmuller₀_mapMonoidHom_idealQuotientMk {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] {x : Perfection R p} : (teichmuller₀ p I) ((mapMonoidHom p ↑(Ideal.Quotient.mk I)) x) = (coeffMonoidHom R p 0) x

theorem Perfection.mk_teichmuller {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] (x : Perfection (R ⧸ I) p) : (Ideal.Quotient.mk I) ((teichmuller p I) x) = (coeff (R ⧸ I) p 0) x

@[simp]

theorem Perfection.mk_teichmuller₀ {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] (x : Perfection (R ⧸ I) p) : (Ideal.Quotient.mk I) ((teichmuller₀ p I) x) = (coeff (R ⧸ I) p 0) x

theorem Perfection.mk_comp_teichmuller (p : ℕ) [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (I : Ideal R) [CharP (R ⧸ I) p] [IsAdicComplete I R] : (↑(Ideal.Quotient.mk I)).comp (teichmuller p I) = ↑(coeff (R ⧸ I) p 0)

theorem Perfection.mk_comp_teichmuller₀ (p : ℕ) [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (I : Ideal R) [CharP (R ⧸ I) p] [IsAdicComplete I R] : (↑(Ideal.Quotient.mk I)).comp (teichmuller₀ p I) = ↑(coeff (R ⧸ I) p 0)

theorem Perfection.mk_comp_teichmuller' (p : ℕ) [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (I : Ideal R) [CharP (R ⧸ I) p] [IsAdicComplete I R] : ⇑(Ideal.Quotient.mk I) ∘ ⇑(teichmuller p I) = ⇑(coeff (R ⧸ I) p 0)

noncomputable def Perfection.quotientMulEquiv (p : ℕ) [Fact (Nat.Prime p)] {R : Type u_2} [CommRing R] (I : Ideal R) [CharP (R ⧸ I) p] [IsAdicComplete I R] : Perfection R p ≃* Perfection (R ⧸ I) p

If R is I-adically complete and R ⧸ I has characteristic p, then Perfection R p and Perfection (R ⧸ I) p are isomorphic as monoids.

Note that Perfection R p is generally not a ring, and the forward map is induced by the quotient map, and the backwards map is constructed using the Teichmüller map.

@[simp]

theorem Perfection.coeff_quotientMulEquiv {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] (x : Perfection R p) (n : ℕ) : (coeff (R ⧸ I) p n) ((quotientMulEquiv p I) x) = (Ideal.Quotient.mk I) ((coeffMonoidHom R p n) x)

@[simp]

theorem Perfection.coeff_zero_symm_quotientMulEquiv {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {I : Ideal R} [CharP (R ⧸ I) p] [IsAdicComplete I R] (x : Perfection (R ⧸ I) p) : (coeffMonoidHom R p 0) ((quotientMulEquiv p I).symm x) = (teichmuller₀ p I) x