[Merged by Bors] - feat(ring_theory/noetherian): fg_pi #10845
Conversation
eric-wieser
commented
Dec 16, 2021
eric-wieser
commented
eric-wieser
added
the
awaiting-review
|
Something like theorem fg_pi {ι : Type*} [fintype ι] {φ : ι → Type*} [Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)] {p : Π (i : ι), submodule R (φ i)} (hsb : ∀ i, (p i).fg) :
(submodule.pi set.univ p).fgshould be true, and more general if I understand |
src/ring_theory/noetherian.lean
Outdated
| @@ -184,6 +184,16 @@ fg_def.2 ⟨linear_map.inl R M P '' tb ∪ linear_map.inr R M P '' tc, | |||
| (htb.1.image _).union (htc.1.image _), | |||
| by rw [linear_map.span_inl_union_inr, htb.2, htc.2]⟩ | |||
|
|
|||
| theorem fg_pi {ι : Type*} [fintype ι] {p : ι → submodule R M} (hsb : ∀ i, (p i).fg) : | |||
There was a problem hiding this comment.
theorem fg_pi {ι : Type*} [fintype ι] {φ : ι → Type*} [Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)] {p : Π (i : ι), submodule R (φ i)} (hsb : ∀ i, (p i).fg) :
(submodule.pi set.univ p).fg
is a more general statement.
There was a problem hiding this comment.
Oh you're quite right, that was careless of me
|
Can you change needs to be manually added to help Lean. |
|
That doesn't work I'm afraid, to make lean happy I need one of these special cases: instance pi' {ι : Type*} {M : Type*} [fintype ι] [non_unital_non_assoc_semiring M]
[module R M] [finite R M] : finite R (ι → M) :=
by apply_instanceinstance pi' {ι : Type*} {M : Type*} [fintype ι] [add_comm_group M]
[module R M] [finite R M] : finite R (ι → M) :=
by apply_instanceWeakening |
|
The first one seems a little weird to me (since a module in general will only have one operation), but the second one is perfectly fine. I think we have finite modules over semiring just because it was for free, but nobody really cares. |
| -- Lean is unable to find this instance without help, either via this `letI`, or via a duplicate | ||
| -- instance with unecessarily strong typeclasses on `R` and `M`. | ||
| letI : module.finite R (fin n.succ → R) := module.finite.pi, |
There was a problem hiding this comment.
This seems like the same problem I was experiencing in #8221, where typeclass search doesn't try hard enough to find the right semiring R and add_comm_monoid arguments that match the module argument it found. Rather than adding a pile of global instances just to be safe, my hope is lean4 will solve this.
| @@ -43,6 +43,10 @@ begin | |||
| { rwa strong_rank_condition_iff_succ R }, | |||
| intros n f, by_contradiction hf, | |||
|
|
|||
| -- Lean is unable to find this instance without help, either via this `letI`, or via a duplicate | |||
| -- instance with unecessarily strong typeclasses on `R` and `M`. | |||
| letI : module.finite R (fin n.succ → R) := module.finite.pi, | |||
There was a problem hiding this comment.
I will let you decide, but I have the impression that it is better to add a global instance that make Lean automatically find this particular one (and maybe others somewhere else).
There was a problem hiding this comment.
Ah, if you think it will be solved in Lean 4 then OK :)
There was a problem hiding this comment.
I hope if lean4 doesn't solve it, we can push for it to be changed so that it does :). I'm not opposed to adding the global instance if we keep running into this, but would prefer to wait for more data and keep things conservative in this PR.
There was a problem hiding this comment.
Yes, this looks like something that could be solved in Lean 4 by solving the metavariables in a smarter order.
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
