feat(ring_theory/algebraic): algebraic extensions, algebraic elements #1519
Conversation
Now this works, and it didn't work previously even with `@` ```lean structure alg_equiv (α β γ : Type*) [comm_ring α] [ring β] [ring γ] [algebra α β] [algebra α γ] extends alg_hom α β γ := ```
| @@ -166,7 +167,7 @@ begin | |||
| rw [finsupp.sum], refine sum_mem _ _, intros r2 hr2, | |||
| rw [finsupp.sum], refine sum_mem _ _, intros r1 hr1, | |||
| rw [algebra.mul_smul_comm, algebra.smul_mul_assoc], | |||
| letI : module ↥S₀ A := _inst_6, refine smul_mem _ _ (smul_mem _ _ _), | |||
| letI hS₀A : module ↥S₀ A := ‹_›, refine smul_mem _ _ (smul_mem _ _ _), | |||
There was a problem hiding this comment.
Getting rid of _inst_6 is certainly an improvement but this could still be clearer. For me it seems to work even without any letI on this line at all.
There was a problem hiding this comment.
I've made some aesthetic changes to this proof. If I delete this particular letI, the proof breaks.
| (S : set (comap R A B)) | ||
| (hS : S = (↑((finset.range (p.nat_degree + 1)).image | ||
| (λ i, to_comap R A B (p.coeff i))) : set (comap R A B))) : | ||
| is_integral (adjoin R S) (comap.to_comap R A B x) := |
There was a problem hiding this comment.
By the way, this lemma is basically trivial and doesn't use A_alg right?
There was a problem hiding this comment.
Yep, I've inlined the include where it's actually needed. And indeed, this lemma is trivial. That's why it has the longest proof (-;
jcommelin
added
the
awaiting-review
| variables {R} | ||
|
|
||
| /-- A subalgebra is algebraic if all its elements are algebraic. -/ | ||
| def subalgebra.is_algebraic (S : subalgebra R A) : Prop := ∀ x ∈ S, is_algebraic R x |
There was a problem hiding this comment.
Is there a reason to introduce is_algebraic for subalgebras first? It looks like "compact subset" again.
Why not just define algebra.is_algebraic directly and then say a subalgebra is algebraic if it is algebraic as an algebra?
There was a problem hiding this comment.
Either way I think you will eventually want to prove that a subalgebra S is algebraic in the sense of algebra.is_algebraic if and only if it is algebraic in the sense of this current subalgebra.is_algebraic (right?). To me algebra.is_algebraic seems like the primary notion so defining it directly looks better.
There was a problem hiding this comment.
More or less done. They now all have elementwise definitions and iffs relating the various definitions.
|
You already had a bunch of comments, so I think it is good to go. |
sgouezel
added
the
ready-to-merge
…leanprover-community#1519) * chore(ring_theory/algebra): make first type argument explicit in alg_hom Now this works, and it didn't work previously even with `@` ```lean structure alg_equiv (α β γ : Type*) [comm_ring α] [ring β] [ring γ] [algebra α β] [algebra α γ] extends alg_hom α β γ := ``` * Update algebra.lean * feat(field_theory/algebraic_closure) * Remove sorries about minimal polynomials * Define alg_equiv.symm * typo * Remove another sorry, in base_extension * Work in progress * Remove a sorry in maximal_extension_chain * Merge two sorries * More sorries removed * More work on transitivity of algebraicity * WIP * Sorry-free definition of algebraic closure * More or less sorries * Removing some sorries * WIP * Fix algebraic.lean * Fix build, mostly * Remove stuff about UMP of alg clos * Prove transitivity of algebraic extensions * Add some docstrings * Remove files with stuff for future PRs * Add a bit to the module docstring * Fix module docstring * Include assumption in section injective * Aesthetic changes to is_integral_of_mem_of_fg * Little improvements of proofs in algebraic.lean * Improve some proofs in integral_closure.lean * Make variable name explicit * Process comments
YaelDillies
removed
the
awaiting-review
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list