define class of ideal lies over

Stream: mathlib4

[Yongle Hu]

Now we have Quotient.algebraQuotientOfLEComap in mathlib, which states that if S is an R-algebra, p and P are ideals of R and S respectively, and P lies over p, then R / p is an S / P-algebra. However, this is a def rather than an instance, since during instance inference, conditions like (h : p ≤ Ideal.comap f P) are not searched for. This brings some difficulties in practice. For example, writing (B ⧸ P) ≃ₐ[A ⧸ p] (B ⧸ P) and Module.Finite (A ⧸ p) (B ⧸ P) results in errors.

To solve it, my current idea is to define a class of lying over. Then we can write (B ⧸ P) ≃ₐ[A ⧸ p] (B ⧸ P) and Module.Finite (A ⧸ p) (B ⧸ P).

import Mathlib.RingTheory.Ideal.Over

variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A)

class ideal_lies_over : Prop where over : p = Ideal.comap (algebraMap A B) P

infix : 50 "lies_over" => ideal_lies_over

variable [ho : P lies_over p]

instance : Algebra (A ⧸ p) (B ⧸ P) := Ideal.Quotient.algebraQuotientOfLEComap (le_of_eq ho.over)

instance : IsScalarTower A (A ⧸ p) (B ⧸ P) := IsScalarTower.of_algebraMap_eq (fun _ ↦ rfl)

instance [Module.Finite A B] : Module.Finite (A ⧸ p) (B ⧸ P) :=
  Module.Finite.of_restrictScalars_finite A (A ⧸ p) (B ⧸ P)

#check (B ⧸ P) ≃ₐ[A ⧸ p] (B ⧸ P)

Is there a better way to solve it? Thanks!

[Kevin Buzzard]

In the FLT repo I demonstrate another solution (which I learnt from Amelia) which is basically just to add the assumption that S/P is an R/p algebra and also to add the IsScalarTower instances for R,R/p,S/P and R,S,S/P. Now you can prove that p is a subset of the pullback of P!

[Yongle Hu]

That's a very clever idea! But the condition I need is p = Ideal.comap (algebraMap A B) P, so using this method, do I need to state p = Ideal.comap (algebraMap A B) P and [Algebra (R ⧸ p) (S ⧸ P)] [IsScalarTower R (R ⧸ p) (S ⧸ P)] at the same time?

[Kevin Buzzard]

I guess this would be one way out of the problem. Your ideal_lies_over solution looks interesting though. I am not really able to judge the relative merits of these approaches.