-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(ring_theory/algebra_tower): Artin--Tate lemma #4282
Conversation
kckennylau
commented
Sep 26, 2020
src/ring_theory/algebra_tower.lean
Outdated
(λ p q _ _ hp hq, hyy $ submodule.mul_mem_mul hp hq) | ||
end | ||
|
||
/- Artin--Tate lemma. Atiyah--Macdonald Proposition 7.8; Stacks 00IS; Altman--Kleiman 16.17. -/ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
/--
instead of /-
? Also, can you explain in the docstring the mathematical content of the theorem, with words?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this looks great. Thanks a lot for doing this.
theorem fg_def {S : subalgebra R A} : S.fg ↔ ∃ t : set A, set.finite t ∧ algebra.adjoin R t = S := | ||
⟨λ ⟨t, ht⟩, ⟨↑t, set.finite_mem_finset t, ht⟩, | ||
λ ⟨t, ht1, ht2⟩, ⟨ht1.to_finset, by rwa set.finite.coe_to_finset⟩⟩ | ||
|
||
theorem fg_bot : (⊥ : subalgebra R A).fg := | ||
⟨∅, algebra.adjoin_empty R A⟩ | ||
|
||
lemma fg_of_submodule_fg (h : (⊤ : submodule R A).fg) : (⊤ : subalgebra R A).fg := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do we want (⊤ : submodule R A).fg)
and (⊤ : subalgebra R A).fg
to be the idomatic way of saying module.finite R A
and algebra.finite R A
? I think I wouldn't mind having those definitions. It looks better, and potentially, those should be classes...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
maybe in a separate PR.
Thanks 🎉 bors merge Ok, let's merge this... but I would really like to see that separate PR. 😺 |
Build failed (retrying...): |
bors r- CI is failing |
Canceled. |
Let's try again bors r+ |
Build failed (retrying...): |
Build failed: |
@kckennylau Could you please take a look at what is wrong? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Pull request successfully merged into master. Build succeeded: |