[Merged by Bors] - feat(ring_theory/perfection): define characteristic predicate of perfection #5386

kckennylau · 2020-12-16T02:35:36Z

Name changes:

perfect_field --> perfect_ring (generalization)
semiring.perfection --> ring.perfection
Original ring.perfection deleted.

…ection

src/field_theory/perfect_closure.lean

src/ring_theory/perfection.lean

Co-authored-by: Johan Commelin <johan@commelin.net>

src/ring_theory/perfection.lean

src/field_theory/perfect_closure.lean

eric-wieser · 2020-12-16T15:15:23Z

src/ring_theory/perfection.lean

-/-- The perfection of a ring `R` with characteristic `p`,
-defined to be the projective limit of `R` using the Frobenius maps `R → R`
-indexed by the natural numbers, implemented as `{ f : ℕ → R | ∀ n, f (n + 1) ^ p = f n }`. -/
-def ring.perfection (R : Type u₁) [comm_ring R] (p : ℕ) [hp : fact p.prime] [char_p R p] :
-  subring (ℕ → R) :=
-{ neg_mem' := λ f hf n, (frobenius_neg R p _).trans $ congr_arg _ (hf n),
-  .. semiring.perfection R p }


What was the rationale for removing this? Is there any other way to obtain this subring without having to repeat the proof here?

The subring isn't important, I just want the type with the ring instance.

But you construct the subring in the other files anyway, don't you?

No, I just prove that the subsemiring is a ring.

jcommelin · 2020-12-18T10:49:13Z

src/ring_theory/perfection.lean

+/-- Given rings `R` and `S` of characteristic `p`, with `R` being perfect,
+any homomorphism `R →+* S` can be extended to a homomorphism `R →+* P`,
+where `P` is any perfection of `S`. -/
+@[simps] noncomputable def extend [perfect_ring R p] (S : Type u₂) [comm_semiring S] [char_p S p]


Should this be called lift?

I don't know any more. its neighbour (K →+* L) ≃ (perfect_closure K p →+* L) is called lift, so I figured this one should be called extend just for the sake of it:

mathlib/src/field_theory/perfect_closure.lean

Lines 382 to 383 in 39ecd1a

def lift (L : Type v) [field L] [char_p L p] [perfect_field L p] :

(K →+* L) ≃ (perfect_closure K p →+* L) :=

Hmm, I would rather call perfect_closure.lift an example of extending something...

Yeah so I figured that we do a switcheroo in Leanspeak

Like Greenland and Iceland.

src/ring_theory/perfection.lean

jcommelin

Thanks 🎉

bors merge

…ection (#5386) Name changes: - `perfect_field` --> `perfect_ring` (generalization) - `semiring.perfection` --> `ring.perfection` - Original `ring.perfection` deleted.

bors · 2020-12-21T10:42:35Z

Canceled.

bryangingechen · 2020-12-21T15:51:13Z

src/ring_theory/perfection.lean

@@ -186,7 +186,7 @@ lemma of : perfection_map p (perfection.coeff R p 0) :=
 mk' (ring_equiv.refl _) $ (equiv.apply_eq_iff_eq_symm_apply _).2 rfl

 /-- For a perfect ring, it itself is the perfection. -/
-def id [perfect_ring R p] : perfection_map p (ring_hom.id R) :=
+lemma id [perfect_ring R p] : perfection_map p (ring_hom.id R) :=


Maybe perfection_map should be renamed to is_perfection_map (in another PR) to make it more clear that it's Prop-valued.

Anyways, the linter is happy now, so let's try again.

bors r+

And just in case...
bors d+

bors · 2020-12-21T15:51:14Z

✌️ kckennylau can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

…ection (#5386) Name changes: - `perfect_field` --> `perfect_ring` (generalization) - `semiring.perfection` --> `ring.perfection` - Original `ring.perfection` deleted.

bors · 2020-12-21T17:48:40Z

Pull request successfully merged into master.

Build succeeded:

kckennylau added 3 commits December 11, 2020 14:21

feat(ring_theory/perfection): define characteristic predicate of perf…

1cb5049

…ection

completed

1e6844c

line length

32a5f30

kckennylau changed the title ~~Perfection~~ feat(ring_theory/perfection): define characteristic predicate of perfection Dec 16, 2020

jcommelin reviewed Dec 16, 2020

View reviewed changes

kckennylau and others added 2 commits December 16, 2020 18:15

Apply suggestions from code review

4724a4d

Co-authored-by: Johan Commelin <johan@commelin.net>

make linter happy

7064226

jcommelin reviewed Dec 16, 2020

View reviewed changes

src/ring_theory/perfection.lean Show resolved Hide resolved

src/ring_theory/perfection.lean Show resolved Hide resolved

coeff_iterate_frobenius'

1fb6df7

eric-wieser reviewed Dec 16, 2020

View reviewed changes

src/field_theory/perfect_closure.lean Show resolved Hide resolved

eric-wieser reviewed Dec 16, 2020

View reviewed changes

bryangingechen added the awaiting-author A reviewer has asked the author a question or requested changes label Dec 16, 2020

unbundle perfection_map

c623391

kckennylau added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Dec 18, 2020

jcommelin reviewed Dec 18, 2020

View reviewed changes

change extend to lift

3372e72

jcommelin approved these changes Dec 21, 2020

View reviewed changes

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Dec 21, 2020

make linter happy

101d561

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Dec 21, 2020

bryangingechen reviewed Dec 21, 2020

View reviewed changes

bryangingechen added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-author A reviewer has asked the author a question or requested changes labels Dec 21, 2020

bors bot changed the title ~~feat(ring_theory/perfection): define characteristic predicate of perfection~~ [Merged by Bors] - feat(ring_theory/perfection): define characteristic predicate of perfection Dec 21, 2020

bors bot closed this Dec 21, 2020

bors bot deleted the perfection branch December 21, 2020 17:48

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(ring_theory/perfection): define characteristic predicate of perfection #5386

[Merged by Bors] - feat(ring_theory/perfection): define characteristic predicate of perfection #5386

kckennylau commented Dec 16, 2020 •

edited

Loading

eric-wieser Dec 16, 2020 •

edited

Loading

kckennylau Dec 17, 2020

eric-wieser Dec 18, 2020

kckennylau Dec 18, 2020

jcommelin Dec 18, 2020

kckennylau Dec 18, 2020

jcommelin Dec 18, 2020

kckennylau Dec 18, 2020

kckennylau Dec 18, 2020

jcommelin left a comment

bors bot commented Dec 21, 2020

bryangingechen Dec 21, 2020

bors bot commented Dec 21, 2020

bors bot commented Dec 21, 2020

	def lift (L : Type v) [field L] [char_p L p] [perfect_field L p] :
	(K →+* L) ≃ (perfect_closure K p →+* L) :=

[Merged by Bors] - feat(ring_theory/perfection): define characteristic predicate of perfection #5386

[Merged by Bors] - feat(ring_theory/perfection): define characteristic predicate of perfection #5386

Conversation

kckennylau commented Dec 16, 2020 • edited Loading

eric-wieser Dec 16, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Dec 21, 2020

Choose a reason for hiding this comment

bors bot commented Dec 21, 2020

bors bot commented Dec 21, 2020

kckennylau commented Dec 16, 2020 •

edited

Loading

eric-wieser Dec 16, 2020 •

edited

Loading