Residue field of HeightOneSpectrum

Stream: Is there code for X?

[Kevin Buzzard]

If $A$ is a Dedekind domain (it's 𝓞 F for F a number field in my application) and if v : HeightOneSpectrum A then what's the way to talk about the residue field of v? Is it just 𝓞 F ⧸ v.asIdeal ? This doesn't seem to have a Field instance...

[Edward van de Meent]

the issue seems to be that Ideal.Quotient.field is not an instance (see docstring for why)

[Yakov Pechersky]

We have docs#Ideal.ResidueField

[Yakov Pechersky]

But that's for the localization, which won't work as well here. You might need to construct your equivalent of docs#IsLocalRing.ResidueField