Theorems · Definition · commutative algebra

Ideal.Quotient.algEquivOfEqComap

{A : Type u_3} →
  {B : Type u_4} →
    {C : Type u_5} →
      [inst : CommRing A] →
        [inst_1 : CommRing B] →
          [inst_2 : CommRing C] →
            [inst_3 : Algebra A B] →
              [inst_4 : Algebra A C] →
                {P : Ideal B} →
                  {Q : Ideal C} →
                    (p : Ideal A) →
                      [inst_5 : Q.LiesOver p] →
                        [inst_6 : P.LiesOver p] →
                          {E : Type u_7} →
                            [inst_7 : EquivLike E B C] →
                              [inst_8 : AlgEquivClass E A B C] → (σ : E) → P = Ideal.comap σ Q → (B ⧸ P) ≃ₐ[A ⧸ p] C ⧸ Q

An A ⧸ p-algebra isomorphism between B ⧸ P and C ⧸ Q induced by an A-algebra isomorphism between B and C, where P = σ⁻¹ Q.

Defined in

Mathlib.RingTheory.Ideal.Over

Cited by

2 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingCommRingAlgebraAlgebraIdeal.LiesOverIdeal.LiesOverEquivLikeAlgEquivClass