The perfect closure of a characteristic p
ring #
Main definitions #
PerfectClosure
: the perfect closure of a characteristicp
ring, which is the smallest extension that makes frobenius surjective.PerfectClosure.mk K p (n, x)
: forn : ℕ
andx : K
this isx ^ (p ^ -n)
viewed as an element ofPerfectClosure K p
. Every element ofPerfectClosure K p
is of this form (PerfectClosure.mk_surjective
).PerfectClosure.of
: the structure map fromK
toPerfectClosure K p
.PerfectClosure.lift
: given a ringK
of characteristicp
and a perfect ringL
of the same characteristic, any homomorphismK →+* L
can be lifted toPerfectClosure K p
.
Main results #
PerfectClosure.induction_on
: to prove a result for all elements of the prefect closure, one only needs to prove it for all elements of the formx ^ (p ^ -n)
.PerfectClosure.mk_mul_mk
,PerfectClosure.one_def
,PerfectClosure.mk_add_mk
,PerfectClosure.neg_mk
,PerfectClosure.zero_def
,PerfectClosure.mk_zero_zero
,PerfectClosure.mk_zero
,PerfectClosure.mk_inv
,PerfectClosure.mk_pow
: how to do multiplication, addition, etc. on elements of formx ^ (p ^ -n)
.PerfectClosure.mk_eq_iff
: when doesx ^ (p ^ -n)
equal.PerfectClosure.eq_iff
: same asPerfectClosure.mk_eq_iff
but with additional assumption thatK
being reduced, hence gives a simpler criterion.PerfectClosure.instPerfectRing
:PerfectClosure K p
is a perfect ring.
Tags #
perfect ring, perfect closure
PerfectClosure.R
is the relation (n, x) ∼ (n + 1, x ^ p)
for n : ℕ
and x : K
.
PerfectClosure K p
is the quotient by this relation.
- intro: ∀ {K : Type u} [inst : CommRing K] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (n : ℕ) (x : K), PerfectClosure.R K p (n, x) (n + 1, (frobenius K p) x)
Instances For
The perfect closure is the smallest extension that makes frobenius surjective.
Equations
- PerfectClosure K p = Quot (PerfectClosure.R K p)
Instances For
PerfectClosure.mk K p (n, x)
for n : ℕ
and x : K
is an element of PerfectClosure K p
,
viewed as x ^ (p ^ -n)
. Every element of PerfectClosure K p
is of this form
(PerfectClosure.mk_surjective
).
Equations
- PerfectClosure.mk K p x = Quot.mk (PerfectClosure.R K p) x
Instances For
Lift a function ℕ × K → L
to a function on PerfectClosure K p
.
Equations
- x.liftOn f hf = Quot.liftOn x f hf
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
Equations
- PerfectClosure.instInhabited K p = { default := 1 }
Equations
- One or more equations did not get rendered due to their size.
Equations
- PerfectClosure.instNeg K p = { neg := Quot.lift (fun (x : ℕ × K) => PerfectClosure.mk K p (x.1, -x.2)) ⋯ }
Equations
- PerfectClosure.instZero K p = { zero := PerfectClosure.mk K p (0, 0) }
Prior to #15862, this lemma was called mk_zero_zero
.
See mk_zero_right
for the lemma used to be called mk_zero
.
Alias of PerfectClosure.mk_zero
.
Prior to #15862, this lemma was called mk_zero_zero
.
See mk_zero_right
for the lemma used to be called mk_zero
.
Equations
Equations
Alias of PerfectClosure.natCast
.
Alias of PerfectClosure.intCast
.
Embedding of K
into PerfectClosure K p
Equations
- PerfectClosure.of K p = { toFun := fun (x : K) => PerfectClosure.mk K p (0, x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Given a ring K
of characteristic p
and a perfect ring L
of the same characteristic,
any homomorphism K →+* L
can be lifted to PerfectClosure K p
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- PerfectClosure.instInv K p = { inv := Quot.lift (fun (x : ℕ × K) => Quot.mk (PerfectClosure.R K p) (x.1, x.2⁻¹)) ⋯ }
Equations
- PerfectClosure.instDivisionRing K p = DivisionRing.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (q : ℚ≥0) => HMul.hMul ↑q) ⋯ ⋯ (fun (q : ℚ) => HMul.hMul ↑q) ⋯
Equations
- PerfectClosure.instField K p = Field.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.nnqsmul ⋯ ⋯ DivisionRing.qsmul ⋯
Equations
- ⋯ = ⋯