Zulip Chat Archive

Stream: general

Topic: Making `ideal.quotient` reducible (or deleted altogether?)

Anne Baanen (Jun 10 2021 at 10:09):

I'm working with ideals that have finite quotients, so my variables look like (I : ideal R) [fintype (ideal.quotient I)]. When I want to apply some lemma defined for submodule quotients, I get a missing instance error for fintype (submodule.quotient I). Since docs#ideal.quotient is defined to equal docs#submodule.quotient, this error goes away if we make ideal.quotient reducible.

Do you know any objection to making ideal.quotient reducible, or even deleting it entirely? (Dot notation is smart enough to interpret I.quotient as submodule.quotient I even if I : ideal R.)

Kevin Buzzard (Jun 10 2021 at 10:38):

First vector spaces, now this :-) I have caught myself in the past writing submodule R R

Last updated: Aug 03 2023 at 10:10 UTC