-
Notifications
You must be signed in to change notification settings - Fork 251
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
feat: generalize finrank_add_finrank_quotient
to PIDs
#9151
Conversation
erdOne
commented
Dec 19, 2023
finrank_add_finrank_quotient
to PIDsfinrank_add_finrank_quotient
to PIDs
@@ -644,6 +644,16 @@ theorem equiv [Finite R M] (e : M ≃ₗ[R] N) : Finite R N := | |||
|
|||
instance ulift [Finite R M] : Finite R (ULift M) := equiv ULift.moduleEquiv.symm | |||
|
|||
theorem iff_FG {N : Submodule R M} : Module.Finite R N ↔ N.FG := Module.finite_def.trans (fg_top _) |
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.
theorem iff_FG {N : Submodule R M} : Module.Finite R N ↔ N.FG := Module.finite_def.trans (fg_top _) | |
theorem iff_fg {N : Submodule R M} : Module.Finite R N ↔ N.FG := Module.finite_def.trans (fg_top _) |
instance [IsDomain R] : NoZeroSMulDivisors R (M ⧸ Submodule.torsion R M) := by | ||
constructor | ||
intros c x hcx | ||
rw [or_iff_not_imp_left] | ||
intro hc | ||
obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x | ||
rw [← LinearMap.map_smul, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at hcx | ||
obtain ⟨n, hn⟩ := hcx | ||
simp only [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, Submonoid.mk_smul, exists_prop] | ||
refine ⟨n * ⟨c, mem_nonZeroDivisors_of_ne_zero hc⟩, ?_⟩ | ||
simpa [Submonoid.smul_def, smul_smul] using hn |
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.
Isn't this exactly Submodule.QuotientTorsion.noZeroSMulDivisors?
instance [IsDomain R] [IsPrincipalIdealRing R] : Module.Free R (M ⧸ Submodule.torsion R M) := | ||
Module.free_of_finite_type_torsion_free' |
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.
Some build failures here and below
lemma FiniteDimensional.finrank_add_finrank_quotient_le (N : Submodule R M) : | ||
finrank R N + finrank R (M ⧸ N) ≤ finrank R M := by |
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.
… results about `Module.rank` in #9151 (#9253) + Proves that `Sup` (ciSup) commutes with cardinal addition (`ciSup_add_ciSup`) and multiplication. Generalize results in Cardinal/Basic introduced in #8842 to achieve this. + Use `ciSup_add_ciSup` to prove that the rank of a module is always at least the rank of a submodule plus the rank of the quotient by the submodule. Deduce that the rank of a product module is at least the sum of the ranks of the two factors. + Show that quotienting by a torsion submodule preserves the rank. + Golf `rank_zero_iff_forall_zero` using a recently added lemma. Co-authored-by: Andrew Yang <the.erd.one@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Closing in favor of #9298 |