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.

source

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.

Equations

x.teichmullerAux 0 = 1
x.teichmullerAux n.succ = Quotient.out ((Perfection.coeff (R ⧸ I) p n) x) ^ p ^ n

Instances For

source

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]

source

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.

Equations

x.teichmullerCauchy = AdicCompletion.AdicCauchySequence.mk I R x.teichmullerAux ⋯

Instances For

source

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 • ⊤]

source

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) :

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.

Equations

x.teichmullerFun = ⋯.choose

Instances For

source

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)]

source

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

source

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

source

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₀.

Equations

Perfection.teichmuller p I = { toFun := Perfection.teichmullerFun, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

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)]

source

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

source

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

source

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

source

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.

Equations

Perfection.teichmuller₀ p I = { toFun := (↑(Perfection.teichmuller p I)).toFun, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

@[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)

source

@[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)

source

@[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)

source

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)]

source

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

source

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

source

@[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

source

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

source

@[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

source

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)

source

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)

source

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)

source

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.

Equations

Perfection.quotientMulEquiv p I = (Perfection.mapMonoidHom p ↑(Ideal.Quotient.mk I)).toMulEquiv ((Perfection.liftMonoidHom p (Perfection (R ⧸ I) p) R) (Perfection.teichmuller p I)) ⋯ ⋯

Instances For

source

@[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)

source

@[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

Documentation

Mathlib.RingTheory.Teichmuller

Teichmüller map #