feat: add Algebra.compHom and related lemma #18404
Conversation
github-actions
bot
added
the
new-contributor
PR summary 988c3ce9eaImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
Can you explain where this will be used? Edit: Or |
|
yhtq
changed the title
Mathlib/Algebra/Algebra/Defs.lean
Outdated
| @@ -175,6 +175,18 @@ def RingHom.toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S) | |||
| smul_def' _ _ := rfl | |||
| toRingHom := i | |||
|
|
|||
| /---/ | |||
There was a problem hiding this comment.
@grunweg, can we have a linter that bans this?
There was a problem hiding this comment.
Yes, that is easy to do (having a linter for doc comments with, say, only whitespace or containing just the string "TODO"). I'll bump it on my list of ideas!
Co-authored-by: Eric Wieser <[email protected]>
| /-- | ||
| Compose a Algebra with a RingHom, with action f s • m. | ||
| -/ |
There was a problem hiding this comment.
| /-- | |
| Compose a Algebra with a RingHom, with action f s • m. | |
| -/ | |
| /-- | |
| Compose an `Algebra` with a `RingHom`, with action `f s • m`. | |
| This is the algebra version of `Module.compHom`. | |
| -/ |
| /-- | ||
| Compose a Algebra with a RingHom, with action f s • m. | ||
| -/ | ||
| abbrev compHom: Algebra S A where |
There was a problem hiding this comment.
style nit:
| abbrev compHom: Algebra S A where | |
| abbrev compHom : Algebra S A where |
Generally, there should always be spaces around colons; can you go through the PR and fix these throughout?
| theorem compHom_smul_def (s : S) (x : A): | ||
| letI := compHom A f | ||
| s • x = f s • x := by | ||
| letI := compHom A f | ||
| rw [Algebra.smul_def] | ||
| exact Eq.symm (smul_def (f s) x) | ||
|
|
||
| theorem compHom_algebraMap_eq : | ||
| letI := compHom A f | ||
| algebraMap S A = (algebraMap R A).comp f := rfl | ||
|
|
||
| theorem compHom_algebraMap_apply (s : S) : | ||
| letI := compHom A f | ||
| algebraMap S A s = (algebraMap R A) (f s) := rfl | ||
|
|
||
| theorem compHom_toRingHom_eq : | ||
| letI := compHom A f | ||
| (compHom A f).toRingHom = (algebraMap R A).comp f := rfl | ||
|
|
||
| theorem compHom_toRingHom_apply (s : S) : | ||
| letI := compHom A f | ||
| (compHom A f).toRingHom s = (algebraMap R A) (f s) := rfl |
There was a problem hiding this comment.
My inclination would be to drop these lemmas; I think since you're using abbrev above, lean will unfold them with dsimp only.
| letI := Algebra.compHom A₂ f | ||
| { | ||
| equiv with | ||
| toFun := equiv, | ||
| invFun := equiv.symm, | ||
| commutes' := by | ||
| simp only [Algebra.compHom_algebraMap_eq, RingHom.coe_comp, Function.comp_apply] | ||
| exact (fun x => (commute x).symm) | ||
| } |
There was a problem hiding this comment.
style nit: This should be indented two spaces not six.
| Define an equivalence of algebras in the following commutative diagram: | ||
| A₁ <------> A₂ | ||
| /\ /\ | ||
| | | | ||
| | | | ||
| S --------> R |
There was a problem hiding this comment.
Can you explain the relation to Algebra.compHom here? Using non-canonical instances like compHom is quite unusual, so it's important to draw attention to it when it happens; especially since the docs wont show the letIs!
Add some simple definition and lemmas to construct Algebra structure from Algebra on another equivalent ring.
As preparation for the following result: If
KandK'are fraction rings ofA, andLandL'are fraction rings ofB, thenIsGalois K LimpliesIsGalois K' L'.