Ideal.Quotient.map

Stream: Is there code for X?

[Kevin Buzzard]

Do we not have this? Surely we must have -- am I just looking in the wrong place? I'd also like an Equiv version where I=J.comap. Also, is the name OK? We have docs#QuotientGroup.lift and docs#QuotientGroup.map, and also docs#Ideal.Quotient.lift . I guess the equiv version should be called Ideal.Quotient.congr to match docs#QuotientGroup.congr (although I don't know why they use maps not comaps in that declaration, comaps don't have a random Exists in)

Asking before PRing because there's a bunch of boilerplate which needs to go with the definition.

import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.RingTheory.Ideal.Maps

variable (R S : Type*) [CommRing R] [CommRing S] (f : R →+* S) (I : Ideal R) (J : Ideal S)

def Ideal.Quotient.map (h : I ≤ J.comap f) : R ⧸ I →+* S ⧸ J :=
  Ideal.Quotient.lift I ((Ideal.Quotient.mk J).comp f) <| fun r hrI ↦ by
  rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem]
  exact h hrI

[Christian Merten]

This is docs#Ideal.quotientMap I believe.

[Christian Merten]

The equiv version is just below: docs#Ideal.quotientEquiv

[Kevin Buzzard]

Many thanks. So perhaps the question is whether the names need thinking about? (if Ideal.Quotient.lift had been called Ideal.quotientLift I would never have even asked). I knew it would be there somewhere. I tried exact? and the docs.

[Kevin Buzzard]

I guess my mistake was assuming that I'd imported enough; exact? does find it but not with the imports I used. I need to replace import Mathlib.RingTheory.Ideal.Quotient with import Mathlib.RingTheory.Ideal.QuotientOperations. I guess this is a consequence of our current "split files a lot to minimise imports" policy and my failure to adapt by putting import Mathlib at the top of a file before exact?.

[Kevin Buzzard]

Can we have exact!? which imports mathlib first?

[Christian Merten]

Kevin Buzzard said:

Many thanks. So perhaps the question is whether the names need thinking about? (if Ideal.Quotient.lift had been called Ideal.quotientLift I would never have even asked). I knew it would be there somewhere. I tried exact? and the docs.

When searching the docs, I find it often useful to drop all .s from the name and search in lower case.

[Kevin Buzzard]

Yes, I know this trick! It also works in VS Code with ctrl-space. I was unfortunately misled in this case by the naming of Ideal.Quotient.lift so didn't try it :-(

[Kim Morrison]

Kevin Buzzard said:

Can we have exact!? which imports mathlib first?

This is perhaps not completely insane. :-) You would have to create a fresh environment with import Mathlib, and then build a new metavariable inside that environment from the Expr for the goal outside that environment. There are probably many ways that could go wrong, but for an exact!? I think it would be fine to make a best effort.

I'm not going to attempt this, but I'd encourage someone to try! (Look around for code using withImportModules as a starting point?)

[Johan Commelin]

Nitpick: shouldn't it be exact?!?

to-mah-to, to-may-to

[Kim Morrison]

I agree exact?! is right, but I've been thinking about chess and liked the "I don't know what I am doing but let me try this." that exact!? suggested. :-)