More operations on modules and ideals related to quotients

Main results:

• RingHom.quotientKerEquivRange : the first isomorphism theorem for commutative rings.
• RingHom.quotientKerEquivRangeS : the first isomorphism theorem for a morphism from a commutative ring to a semiring.
• AlgHom.quotientKerEquivRange : the first isomorphism theorem for a morphism of algebras (over a commutative semiring)
• RingHom.quotientKerEquivRangeS : the first isomorphism theorem for a morphism from a commutative ring to a semiring.
• Ideal.quotientInfRingEquivPiQuotient: the Chinese Remainder Theorem, version for coprime ideals (see also ZMod.prodEquivPi in Data.ZMod.Quotient for elementary versions about ZMod).

def RingHom.kerLift {R : Type u} {S : Type v} [CommRing R] [Semiring S] (f : R →+* S) : R ⧸ RingHom.ker f →+* S

The induced map from the quotient by the kernel to the codomain.

This is an isomorphism if f has a right inverse (quotientKerEquivOfRightInverse) / is surjective (quotientKerEquivOfSurjective).

Equations

• f.kerLift = Ideal.Quotient.lift (RingHom.ker f) f ⋯

@[simp]

theorem RingHom.kerLift_mk {R : Type u} {S : Type v} [CommRing R] [Semiring S] (f : R →+* S) (r : R) : f.kerLift ((Ideal.Quotient.mk (RingHom.ker f)) r) = f r

theorem RingHom.lift_injective_of_ker_le_ideal {R : Type u} {S : Type v} [CommRing R] [Semiring S] (I : Ideal R) {f : R →+* S} (H : ∀ a ∈ I, f a = 0) (hI : RingHom.ker f ≤ I) : Function.Injective ⇑(Ideal.Quotient.lift I f H)

theorem RingHom.kerLift_injective {R : Type u} {S : Type v} [CommRing R] [Semiring S] (f : R →+* S) : Function.Injective ⇑f.kerLift

The induced map from the quotient by the kernel is injective.

def RingHom.quotientKerEquivOfRightInverse {R : Type u} {S : Type v} [CommRing R] [Semiring S] {f : R →+* S} {g : S → R} (hf : Function.RightInverse g ⇑f) : R ⧸ RingHom.ker f ≃+* S

The first isomorphism theorem for commutative rings, computable version.

Equations

• RingHom.quotientKerEquivOfRightInverse hf = { toFun := ⇑f.kerLift, invFun := ⇑(Ideal.Quotient.mk (RingHom.ker f)) ∘ g, left_inv := ⋯, right_inv := hf, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingHom.quotientKerEquivOfRightInverse.apply {R : Type u} {S : Type v} [CommRing R] [Semiring S] {f : R →+* S} {g : S → R} (hf : Function.RightInverse g ⇑f) (x : R ⧸ RingHom.ker f) : (RingHom.quotientKerEquivOfRightInverse hf) x = f.kerLift x

@[simp]

theorem RingHom.quotientKerEquivOfRightInverse.Symm.apply {R : Type u} {S : Type v} [CommRing R] [Semiring S] {f : R →+* S} {g : S → R} (hf : Function.RightInverse g ⇑f) (x : S) : (RingHom.quotientKerEquivOfRightInverse hf).symm x = (Ideal.Quotient.mk (RingHom.ker f)) (g x)

def RingEquiv.quotientBot (R : Type u) [CommRing R] : R ⧸ ⊥ ≃+* R

The quotient of a ring by he zero ideal is isomorphic to the ring itself.

Equations

• RingEquiv.quotientBot R = (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfRightInverse ⋯)

noncomputable def RingHom.quotientKerEquivOfSurjective {R : Type u} {S : Type v} [CommRing R] [Semiring S] {f : R →+* S} (hf : Function.Surjective ⇑f) : R ⧸ RingHom.ker f ≃+* S

The first isomorphism theorem for commutative rings, surjective case.

Equations

• RingHom.quotientKerEquivOfSurjective hf = RingHom.quotientKerEquivOfRightInverse ⋯

noncomputable def RingHom.quotientKerEquivRangeS {R : Type u} {S : Type v} [CommRing R] [Semiring S] (f : R →+* S) : R ⧸ RingHom.ker f ≃+* ↥f.rangeS

The first isomorphism theorem for commutative rings (RingHom.rangeS version).

Equations

• f.quotientKerEquivRangeS = (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfSurjective ⋯)

noncomputable def RingHom.quotientKerEquivRange {R : Type u} [CommRing R] {S : Type v} [Ring S] (f : R →+* S) : R ⧸ RingHom.ker f ≃+* ↥f.range

The first isomorphism theorem for commutative rings (RingHom.range version).

Equations

• f.quotientKerEquivRange = (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfSurjective ⋯)

@[simp]

theorem Ideal.map_quotient_self {R : Type u} [CommRing R] (I : Ideal R) : Ideal.map (Ideal.Quotient.mk I) I = ⊥

@[simp]

theorem Ideal.mk_ker {R : Type u} [CommRing R] {I : Ideal R} : RingHom.ker (Ideal.Quotient.mk I) = I

theorem Ideal.map_mk_eq_bot_of_le {R : Type u} [CommRing R] {I J : Ideal R} (h : I ≤ J) : Ideal.map (Ideal.Quotient.mk J) I = ⊥

theorem Ideal.ker_quotient_lift {R : Type u} {S : Type v} [CommRing R] [Semiring S] {I : Ideal R} (f : R →+* S) (H : I ≤ RingHom.ker f) : RingHom.ker (Ideal.Quotient.lift I f H) = Ideal.map (Ideal.Quotient.mk I) (RingHom.ker f)

theorem Ideal.injective_lift_iff {R : Type u} {S : Type v} [CommRing R] [Semiring S] {I : Ideal R} {f : R →+* S} (H : ∀ a ∈ I, f a = 0) : Function.Injective ⇑(Ideal.Quotient.lift I f H) ↔ RingHom.ker f = I

theorem Ideal.ker_Pi_Quotient_mk {R : Type u} [CommRing R] {ι : Type u_1} (I : ι → Ideal R) : RingHom.ker (Pi.ringHom fun (i : ι) => Ideal.Quotient.mk (I i)) = ⨅ (i : ι), I i

@[simp]

theorem Ideal.bot_quotient_isMaximal_iff {R : Type u} [CommRing R] (I : Ideal R) : ⊥.IsMaximal ↔ I.IsMaximal

@[simp]

theorem Ideal.mem_quotient_iff_mem_sup {R : Type u} [CommRing R] {I J : Ideal R} {x : R} : (Ideal.Quotient.mk I) x ∈ Ideal.map (Ideal.Quotient.mk I) J ↔ x ∈ J ⊔ I

See also Ideal.mem_quotient_iff_mem in case I ≤ J.

theorem Ideal.mem_quotient_iff_mem {R : Type u} [CommRing R] {I J : Ideal R} (hIJ : I ≤ J) {x : R} : (Ideal.Quotient.mk I) x ∈ Ideal.map (Ideal.Quotient.mk I) J ↔ x ∈ J

See also Ideal.mem_quotient_iff_mem_sup if the assumption I ≤ J is not available.

def Ideal.quotientInfToPiQuotient {R : Type u} [CommRing R] {ι : Type u_1} (I : ι → Ideal R) : R ⧸ ⨅ (i : ι), I i →+* (i : ι) → R ⧸ I i

The homomorphism from R/(⋂ i, f i) to ∏ i, (R / f i) featured in the Chinese Remainder Theorem. It is bijective if the ideals f i are coprime.

Equations

• Ideal.quotientInfToPiQuotient I = Ideal.Quotient.lift (⨅ (i : ι), I i) (Pi.ringHom fun (i : ι) => Ideal.Quotient.mk (I i)) ⋯

theorem Ideal.quotientInfToPiQuotient_mk {R : Type u} [CommRing R] {ι : Type u_1} (I : ι → Ideal R) (x : R) : (Ideal.quotientInfToPiQuotient I) ((Ideal.Quotient.mk (⨅ (i : ι), I i)) x) = fun (i : ι) => (Ideal.Quotient.mk (I i)) x

theorem Ideal.quotientInfToPiQuotient_mk' {R : Type u} [CommRing R] {ι : Type u_1} (I : ι → Ideal R) (x : R) (i : ι) : (Ideal.quotientInfToPiQuotient I) ((Ideal.Quotient.mk (⨅ (i : ι), I i)) x) i = (Ideal.Quotient.mk (I i)) x

theorem Ideal.quotientInfToPiQuotient_inj {R : Type u} [CommRing R] {ι : Type u_1} (I : ι → Ideal R) : Function.Injective ⇑(Ideal.quotientInfToPiQuotient I)

theorem Ideal.quotientInfToPiQuotient_surj {R : Type u} [CommRing R] {ι : Type u_1} [Finite ι] {I : ι → Ideal R} (hI : Pairwise (IsCoprime on I)) : Function.Surjective ⇑(Ideal.quotientInfToPiQuotient I)

noncomputable def Ideal.quotientInfRingEquivPiQuotient {R : Type u} [CommRing R] {ι : Type u_1} [Finite ι] (f : ι → Ideal R) (hf : Pairwise (IsCoprime on f)) : R ⧸ ⨅ (i : ι), f i ≃+* ((i : ι) → R ⧸ f i)

Chinese Remainder Theorem. Eisenbud Ex.2.6. Similar to Atiyah-Macdonald 1.10 and Stacks 00DT

Equations

• Ideal.quotientInfRingEquivPiQuotient f hf = { toEquiv := Equiv.ofBijective ⇑(Ideal.quotientInfToPiQuotient f) ⋯, map_mul' := ⋯, map_add' := ⋯ }

theorem Ideal.pi_quotient_surjective {R : Type u_2} [CommRing R] {ι : Type u_3} [Finite ι] {I : ι → Ideal R} (hf : Pairwise fun (i j : ι) => IsCoprime (I i) (I j)) (x : (i : ι) → R ⧸ I i) : ∃ (r : R), ∀ (i : ι), (Ideal.Quotient.mk (I i)) r = x i

Corollary of Chinese Remainder Theorem: if Iᵢ are pairwise coprime ideals in a commutative ring then the canonical map R → ∏ (R ⧸ Iᵢ) is surjective.

theorem Ideal.exists_forall_sub_mem_ideal {R : Type u_2} [CommRing R] {ι : Type u_3} [Finite ι] {I : ι → Ideal R} (hI : Pairwise fun (i j : ι) => IsCoprime (I i) (I j)) (x : ι → R) : ∃ (r : R), ∀ (i : ι), r - x i ∈ I i

Corollary of Chinese Remainder Theorem: if Iᵢ are pairwise coprime ideals in a commutative ring then given elements xᵢ you can find r with r - xᵢ ∈ Iᵢ for all i.

noncomputable def Ideal.quotientInfEquivQuotientProd {R : Type u} [CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) : R ⧸ I ⊓ J ≃+* (R ⧸ I) × R ⧸ J

Chinese remainder theorem, specialized to two ideals.

Equations

• I.quotientInfEquivQuotientProd J coprime = (Ideal.quotEquivOfEq ⋯).trans ((Ideal.quotientInfRingEquivPiQuotient ![I, J] ⋯).trans (RingEquiv.piFinTwo fun (i : Fin 2) => R ⧸ ![I, J] i))

@[simp]

theorem Ideal.quotientInfEquivQuotientProd_fst {R : Type u} [CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I ⊓ J) : ((I.quotientInfEquivQuotientProd J coprime) x).1 = (Ideal.Quotient.factor (I ⊓ J) I ⋯) x

@[simp]

theorem Ideal.quotientInfEquivQuotientProd_snd {R : Type u} [CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I ⊓ J) : ((I.quotientInfEquivQuotientProd J coprime) x).2 = (Ideal.Quotient.factor (I ⊓ J) J ⋯) x

@[simp]

theorem Ideal.fst_comp_quotientInfEquivQuotientProd {R : Type u} [CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) : (RingHom.fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime) = Ideal.Quotient.factor (I ⊓ J) I ⋯

@[simp]

theorem Ideal.snd_comp_quotientInfEquivQuotientProd {R : Type u} [CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) : (RingHom.snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime) = Ideal.Quotient.factor (I ⊓ J) J ⋯

noncomputable def Ideal.quotientMulEquivQuotientProd {R : Type u} [CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) : R ⧸ I * J ≃+* (R ⧸ I) × R ⧸ J

Chinese remainder theorem, specialized to two ideals.

Equations

• I.quotientMulEquivQuotientProd J coprime = (Ideal.quotEquivOfEq ⋯).trans (I.quotientInfEquivQuotientProd J coprime)

@[simp]

theorem Ideal.quotientMulEquivQuotientProd_fst {R : Type u} [CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I * J) : ((I.quotientMulEquivQuotientProd J coprime) x).1 = (Ideal.Quotient.factor (I * J) I ⋯) x

@[simp]

theorem Ideal.quotientMulEquivQuotientProd_snd {R : Type u} [CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I * J) : ((I.quotientMulEquivQuotientProd J coprime) x).2 = (Ideal.Quotient.factor (I * J) J ⋯) x

@[simp]

theorem Ideal.fst_comp_quotientMulEquivQuotientProd {R : Type u} [CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) : (RingHom.fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime) = Ideal.Quotient.factor (I * J) I ⋯

@[simp]

theorem Ideal.snd_comp_quotientMulEquivQuotientProd {R : Type u} [CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) : (RingHom.snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime) = Ideal.Quotient.factor (I * J) J ⋯

instance Ideal.Quotient.algebra (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] {I : Ideal A} : Algebra R₁ (A ⧸ I)

The R₁-algebra structure on A/I for an R₁-algebra A

Equations

• Ideal.Quotient.algebra R₁ = Algebra.mk ((Ideal.Quotient.mk I).comp (algebraMap R₁ A)) ⋯ ⋯

instance Ideal.Quotient.isScalarTower (R₁ : Type u_1) (R₂ : Type u_2) {A : Type u_3} [CommSemiring R₁] [CommSemiring R₂] [CommRing A] [Algebra R₁ A] [Algebra R₂ A] [SMul R₁ R₂] [IsScalarTower R₁ R₂ A] (I : Ideal A) : IsScalarTower R₁ R₂ (A ⧸ I)

def Ideal.Quotient.mkₐ (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) : A →ₐ[R₁] A ⧸ I

The canonical morphism A →ₐ[R₁] A ⧸ I as morphism of R₁-algebras, for I an ideal of A, where A is an R₁-algebra.

Equations

• Ideal.Quotient.mkₐ R₁ I = { toFun := fun (a : A) => Submodule.Quotient.mk a, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem Ideal.Quotient.algHom_ext (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] {I : Ideal A} {S : Type u_5} [Semiring S] [Algebra R₁ S] ⦃f g : A ⧸ I →ₐ[R₁] S⦄ (h : f.comp (Ideal.Quotient.mkₐ R₁ I) = g.comp (Ideal.Quotient.mkₐ R₁ I)) : f = g

theorem Ideal.Quotient.alg_map_eq (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) : algebraMap R₁ (A ⧸ I) = (algebraMap A (A ⧸ I)).comp (algebraMap R₁ A)

theorem Ideal.Quotient.mkₐ_toRingHom (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) : (Ideal.Quotient.mkₐ R₁ I).toRingHom = Ideal.Quotient.mk I

@[simp]

theorem Ideal.Quotient.mkₐ_eq_mk (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) : ⇑(Ideal.Quotient.mkₐ R₁ I) = ⇑(Ideal.Quotient.mk I)

@[simp]

theorem Ideal.Quotient.algebraMap_eq {R : Type u} [CommRing R] (I : Ideal R) : algebraMap R (R ⧸ I) = Ideal.Quotient.mk I

@[simp]

theorem Ideal.Quotient.mk_comp_algebraMap (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) : (Ideal.Quotient.mk I).comp (algebraMap R₁ A) = algebraMap R₁ (A ⧸ I)

@[simp]

theorem Ideal.Quotient.mk_algebraMap (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) (x : R₁) : (Ideal.Quotient.mk I) ((algebraMap R₁ A) x) = (algebraMap R₁ (A ⧸ I)) x

theorem Ideal.Quotient.mkₐ_surjective (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) : Function.Surjective ⇑(Ideal.Quotient.mkₐ R₁ I)

The canonical morphism A →ₐ[R₁] I.quotient is surjective.

@[simp]

theorem Ideal.Quotient.mkₐ_ker (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] (I : Ideal A) : RingHom.ker ↑(Ideal.Quotient.mkₐ R₁ I) = I

The kernel of A →ₐ[R₁] I.quotient is I.

def Ideal.Quotient.liftₐ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (I : Ideal A) (f : A →ₐ[R₁] B) (hI : ∀ a ∈ I, f a = 0) : A ⧸ I →ₐ[R₁] B

Ideal.quotient.lift as an AlgHom.

Equations

• Ideal.Quotient.liftₐ I f hI = { toRingHom := Ideal.Quotient.lift I (↑f) hI, commutes' := ⋯ }

@[simp]

theorem Ideal.Quotient.liftₐ_apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (I : Ideal A) (f : A →ₐ[R₁] B) (hI : ∀ a ∈ I, f a = 0) (x : A ⧸ I) : (Ideal.Quotient.liftₐ I f hI) x = (Ideal.Quotient.lift I (↑f) hI) x

theorem Ideal.Quotient.liftₐ_comp {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (I : Ideal A) (f : A →ₐ[R₁] B) (hI : ∀ a ∈ I, f a = 0) : (Ideal.Quotient.liftₐ I f hI).comp (Ideal.Quotient.mkₐ R₁ I) = f

theorem Ideal.KerLift.map_smul {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (f : A →ₐ[R₁] B) (r : R₁) (x : A ⧸ RingHom.ker f) : f.kerLift (r • x) = r • f.kerLift x

def Ideal.kerLiftAlg {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (f : A →ₐ[R₁] B) : A ⧸ RingHom.ker f →ₐ[R₁] B

The induced algebras morphism from the quotient by the kernel to the codomain.

This is an isomorphism if f has a right inverse (quotientKerAlgEquivOfRightInverse) / is surjective (quotientKerAlgEquivOfSurjective).

Equations

• Ideal.kerLiftAlg f = AlgHom.mk' (↑f).kerLift ⋯

@[simp]

theorem Ideal.kerLiftAlg_mk {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (f : A →ₐ[R₁] B) (a : A) : (Ideal.kerLiftAlg f) ((Ideal.Quotient.mk (RingHom.ker f)) a) = f a

@[simp]

theorem Ideal.kerLiftAlg_toRingHom {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (f : A →ₐ[R₁] B) : ↑(Ideal.kerLiftAlg f) = (↑f).kerLift

theorem Ideal.kerLiftAlg_injective {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] (f : A →ₐ[R₁] B) : Function.Injective ⇑(Ideal.kerLiftAlg f)

The induced algebra morphism from the quotient by the kernel is injective.

def Ideal.quotientKerAlgEquivOfRightInverse {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : B → A} (hf : Function.RightInverse g ⇑f) : (A ⧸ RingHom.ker f) ≃ₐ[R₁] B

The first isomorphism theorem for algebras, computable version.

Equations

• Ideal.quotientKerAlgEquivOfRightInverse hf = { toEquiv := (RingHom.quotientKerEquivOfRightInverse hf).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Ideal.quotientKerAlgEquivOfRightInverse_apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : B → A} (hf : Function.RightInverse g ⇑f) (a : A ⧸ RingHom.ker f.toRingHom) : (Ideal.quotientKerAlgEquivOfRightInverse hf) a = (↑f).kerLift a

@[simp]

theorem Ideal.quotientKerAlgEquivOfRightInverse_symm_apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : B → A} (hf : Function.RightInverse g ⇑f) (a✝ : B) : (Ideal.quotientKerAlgEquivOfRightInverse hf).symm a✝ = (Ideal.Quotient.mk (RingHom.ker ↑f)) (g a✝)

@[deprecated Ideal.quotientKerAlgEquivOfRightInverse_apply]

theorem Ideal.quotientKerAlgEquivOfRightInverse.apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : B → A} (hf : Function.RightInverse g ⇑f) (a : A ⧸ RingHom.ker f.toRingHom) : (Ideal.quotientKerAlgEquivOfRightInverse hf) a = (↑f).kerLift a

Alias of Ideal.quotientKerAlgEquivOfRightInverse_apply.

@[deprecated Ideal.quotientKerAlgEquivOfRightInverse_symm_apply]

theorem Ideal.QuotientKerAlgEquivOfRightInverseSymm.apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} {g : B → A} (hf : Function.RightInverse g ⇑f) (a✝ : B) : (Ideal.quotientKerAlgEquivOfRightInverse hf).symm a✝ = (Ideal.Quotient.mk (RingHom.ker ↑f)) (g a✝)

Alias of Ideal.quotientKerAlgEquivOfRightInverse_symm_apply.

noncomputable def Ideal.quotientKerAlgEquivOfSurjective {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} (hf : Function.Surjective ⇑f) : (A ⧸ RingHom.ker f) ≃ₐ[R₁] B

The first isomorphism theorem for algebras.

Equations

• Ideal.quotientKerAlgEquivOfSurjective hf = Ideal.quotientKerAlgEquivOfRightInverse ⋯

@[simp]

theorem Ideal.quotientKerAlgEquivOfSurjective_apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} (hf : Function.Surjective ⇑f) (a : A ⧸ RingHom.ker f.toRingHom) : (Ideal.quotientKerAlgEquivOfSurjective hf) a = (↑f).kerLift a

@[simp]

theorem Ideal.quotientKerAlgEquivOfSurjective_symm_apply {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [Semiring B] [Algebra R₁ B] {f : A →ₐ[R₁] B} (hf : Function.Surjective ⇑f) (a✝ : B) : (Ideal.quotientKerAlgEquivOfSurjective hf).symm a✝ = (Ideal.Quotient.mk (RingHom.ker ↑f)) (Classical.choose ⋯ a✝)

def Ideal.quotientMap {R : Type u} [CommRing R] {S : Type v} [CommRing S] {I : Ideal R} (J : Ideal S) (f : R →+* S) (hIJ : I ≤ Ideal.comap f J) : R ⧸ I →+* S ⧸ J

The ring hom R/I →+* S/J induced by a ring hom f : R →+* S with I ≤ f⁻¹(J)

Equations

• Ideal.quotientMap J f hIJ = Ideal.Quotient.lift I ((Ideal.Quotient.mk J).comp f) ⋯

@[simp]

theorem Ideal.quotientMap_mk {R : Type u} [CommRing R] {S : Type v} [CommRing S] {J : Ideal R} {I : Ideal S} {f : R →+* S} {H : J ≤ Ideal.comap f I} {x : R} : (Ideal.quotientMap I f H) ((Ideal.Quotient.mk J) x) = (Ideal.Quotient.mk I) (f x)

@[simp]

theorem Ideal.quotientMap_algebraMap {R₁ : Type u_1} {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] {S : Type v} [CommRing S] {J : Ideal A} {I : Ideal S} {f : A →+* S} {H : J ≤ Ideal.comap f I} {x : R₁} : (Ideal.quotientMap I f H) ((algebraMap R₁ (A ⧸ J)) x) = (Ideal.Quotient.mk I) (f ((algebraMap R₁ A) x))

theorem Ideal.quotientMap_comp_mk {R : Type u} [CommRing R] {S : Type v} [CommRing S] {J : Ideal R} {I : Ideal S} {f : R →+* S} (H : J ≤ Ideal.comap f I) : (Ideal.quotientMap I f H).comp (Ideal.Quotient.mk J) = (Ideal.Quotient.mk I).comp f

theorem Ideal.ker_quotientMap_mk {R : Type u} [CommRing R] {I J : Ideal R} : RingHom.ker (Ideal.quotientMap (Ideal.map (Ideal.Quotient.mk I) J) (Ideal.Quotient.mk I) ⋯) = Ideal.map (Ideal.Quotient.mk J) I

def Ideal.quotientEquiv {R : Type u} [CommRing R] {S : Type v} [CommRing S] (I : Ideal R) (J : Ideal S) (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) : R ⧸ I ≃+* S ⧸ J

The ring equiv R/I ≃+* S/J induced by a ring equiv f : R ≃+* S, where J = f(I).

Equations

• I.quotientEquiv J f hIJ = { toFun := (↑↑(Ideal.quotientMap J ↑f ⋯)).toFun, invFun := ⇑(Ideal.quotientMap I ↑f.symm ⋯), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem Ideal.quotientEquiv_apply {R : Type u} [CommRing R] {S : Type v} [CommRing S] (I : Ideal R) (J : Ideal S) (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) (a✝ : R ⧸ I) : (I.quotientEquiv J f hIJ) a✝ = (↑↑(Ideal.quotientMap J ↑f ⋯)).toFun a✝

@[simp]

theorem Ideal.quotientEquiv_symm_apply {R : Type u} [CommRing R] {S : Type v} [CommRing S] (I : Ideal R) (J : Ideal S) (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) (a : S ⧸ J) : (I.quotientEquiv J f hIJ).symm a = (Ideal.quotientMap I ↑f.symm ⋯) a

theorem Ideal.quotientEquiv_mk {R : Type u} [CommRing R] {S : Type v} [CommRing S] (I : Ideal R) (J : Ideal S) (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) (x : R) : (I.quotientEquiv J f hIJ) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk J) (f x)

@[simp]

theorem Ideal.quotientEquiv_symm_mk {R : Type u} [CommRing R] {S : Type v} [CommRing S] (I : Ideal R) (J : Ideal S) (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) (x : S) : (I.quotientEquiv J f hIJ).symm ((Ideal.Quotient.mk J) x) = (Ideal.Quotient.mk I) (f.symm x)

theorem Ideal.quotientMap_injective' {R : Type u} [CommRing R] {S : Type v} [CommRing S] {J : Ideal R} {I : Ideal S} {f : R →+* S} {H : J ≤ Ideal.comap f I} (h : Ideal.comap f I ≤ J) : Function.Injective ⇑(Ideal.quotientMap I f H)

H and h are kept as separate hypothesis since H is used in constructing the quotient map.

theorem Ideal.quotientMap_injective {R : Type u} [CommRing R] {S : Type v} [CommRing S] {I : Ideal S} {f : R →+* S} : Function.Injective ⇑(Ideal.quotientMap I f ⋯)

If we take J = I.comap f then quotientMap is injective automatically.

theorem Ideal.quotientMap_surjective {R : Type u} [CommRing R] {S : Type v} [CommRing S] {J : Ideal R} {I : Ideal S} {f : R →+* S} {H : J ≤ Ideal.comap f I} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(Ideal.quotientMap I f H)

theorem Ideal.comp_quotientMap_eq_of_comp_eq {R : Type u} [CommRing R] {S : Type v} [CommRing S] {R' : Type u_5} {S' : Type u_6} [CommRing R'] [CommRing S'] {f : R →+* S} {f' : R' →+* S'} {g : R →+* R'} {g' : S →+* S'} (hfg : f'.comp g = g'.comp f) (I : Ideal S') : let leq := ⋯; (Ideal.quotientMap I g' ⋯).comp (Ideal.quotientMap (Ideal.comap g' I) f ⋯) = (Ideal.quotientMap I f' ⋯).comp (Ideal.quotientMap (Ideal.comap f' I) g leq)

Commutativity of a square is preserved when taking quotients by an ideal.

def Ideal.quotientMapₐ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [CommRing B] [Algebra R₁ B] {I : Ideal A} (J : Ideal B) (f : A →ₐ[R₁] B) (hIJ : I ≤ Ideal.comap f J) : A ⧸ I →ₐ[R₁] B ⧸ J

The algebra hom A/I →+* B/J induced by an algebra hom f : A →ₐ[R₁] B with I ≤ f⁻¹(J).

Equations

• Ideal.quotientMapₐ J f hIJ = { toRingHom := Ideal.quotientMap J (↑f) hIJ, commutes' := ⋯ }

@[simp]

theorem Ideal.quotient_map_mkₐ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [CommRing B] [Algebra R₁ B] {I : Ideal A} (J : Ideal B) (f : A →ₐ[R₁] B) (H : I ≤ Ideal.comap f J) {x : A} : (Ideal.quotientMapₐ J f H) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mkₐ R₁ J) (f x)

theorem Ideal.quotient_map_comp_mkₐ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [CommRing B] [Algebra R₁ B] {I : Ideal A} (J : Ideal B) (f : A →ₐ[R₁] B) (H : I ≤ Ideal.comap f J) : (Ideal.quotientMapₐ J f H).comp (Ideal.Quotient.mkₐ R₁ I) = (Ideal.Quotient.mkₐ R₁ J).comp f

def Ideal.quotientEquivAlg {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] [CommRing B] [Algebra R₁ B] (I : Ideal A) (J : Ideal B) (f : A ≃ₐ[R₁] B) (hIJ : J = Ideal.map (↑f) I) : (A ⧸ I) ≃ₐ[R₁] B ⧸ J

The algebra equiv A/I ≃ₐ[R] B/J induced by an algebra equiv f : A ≃ₐ[R] B, whereJ = f(I).

Equations

• I.quotientEquivAlg J f hIJ = { toEquiv := (I.quotientEquiv J (↑f) hIJ).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[reducible, inline]

abbrev Ideal.Quotient.algebraQuotientOfLEComap {R : Type u} [CommRing R] {A : Type u_3} [CommRing A] [Algebra R A] {p : Ideal R} {P : Ideal A} (h : p ≤ Ideal.comap (algebraMap R A) P) : Algebra (R ⧸ p) (A ⧸ P)

If P lies over p, then R / p has a canonical map to A / P.

Equations

• Ideal.Quotient.algebraQuotientOfLEComap h = Algebra.mk (Ideal.quotientMap P (algebraMap R A) h) ⋯ ⋯

@[instance 100]

instance Ideal.quotientAlgebra {R : Type u} [CommRing R] {A : Type u_3} [CommRing A] {I : Ideal A} [Algebra R A] : Algebra (R ⧸ Ideal.comap (algebraMap R A) I) (A ⧸ I)

Equations

• Ideal.quotientAlgebra = Ideal.Quotient.algebraQuotientOfLEComap ⋯

theorem Ideal.algebraMap_quotient_injective {R : Type u} [CommRing R] {A : Type u_3} [CommRing A] {I : Ideal A} [Algebra R A] : Function.Injective ⇑(algebraMap (R ⧸ Ideal.comap (algebraMap R A) I) (A ⧸ I))

def Ideal.quotientEquivAlgOfEq (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] {I J : Ideal A} (h : I = J) : (A ⧸ I) ≃ₐ[R₁] A ⧸ J

Quotienting by equal ideals gives equivalent algebras.

Equations

• Ideal.quotientEquivAlgOfEq R₁ h = I.quotientEquivAlg J AlgEquiv.refl ⋯

@[simp]

theorem Ideal.quotientEquivAlgOfEq_mk (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] {I J : Ideal A} (h : I = J) (x : A) : (Ideal.quotientEquivAlgOfEq R₁ h) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk J) x

@[simp]

theorem Ideal.quotientEquivAlgOfEq_symm (R₁ : Type u_1) {A : Type u_3} [CommSemiring R₁] [CommRing A] [Algebra R₁ A] {I J : Ideal A} (h : I = J) : (Ideal.quotientEquivAlgOfEq R₁ h).symm = Ideal.quotientEquivAlgOfEq R₁ ⋯

theorem Ideal.comap_map_mk {R : Type u} [CommRing R] {I J : Ideal R} (h : I ≤ J) : Ideal.comap (Ideal.Quotient.mk I) (Ideal.map (Ideal.Quotient.mk I) J) = J

noncomputable def Ideal.quotientKerEquivRange {R : Type u} [CommRing R] {A : Type u_5} {B : Type u_6} [CommRing A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) : (A ⧸ RingHom.ker f) ≃ₐ[R] ↥f.range

The first isomorphism theorem for commutative algebras (AlgHom.range version).

Equations

• Ideal.quotientKerEquivRange f = (Ideal.quotientEquivAlgOfEq R ⋯).trans (Ideal.quotientKerAlgEquivOfSurjective ⋯)

def DoubleQuot.quotLeftToQuotSup {R : Type u} [CommRing R] (I J : Ideal R) : R ⧸ I →+* R ⧸ I ⊔ J

The obvious ring hom R/I → R/(I ⊔ J)

Equations

• DoubleQuot.quotLeftToQuotSup I J = Ideal.Quotient.factor I (I ⊔ J) ⋯

theorem DoubleQuot.ker_quotLeftToQuotSup {R : Type u} [CommRing R] (I J : Ideal R) : RingHom.ker (DoubleQuot.quotLeftToQuotSup I J) = Ideal.map (Ideal.Quotient.mk I) J

The kernel of quotLeftToQuotSup

def DoubleQuot.quotQuotToQuotSup {R : Type u} [CommRing R] (I J : Ideal R) : (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →+* R ⧸ I ⊔ J

The ring homomorphism (R/I)/J' -> R/(I ⊔ J) induced by quotLeftToQuotSup where J' is the image of J in R/I

Equations

• DoubleQuot.quotQuotToQuotSup I J = Ideal.Quotient.lift (Ideal.map (Ideal.Quotient.mk I) J) (DoubleQuot.quotLeftToQuotSup I J) ⋯

def DoubleQuot.quotQuotMk {R : Type u} [CommRing R] (I J : Ideal R) : R →+* (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J

The composite of the maps R → (R/I) and (R/I) → (R/I)/J'

Equations

• DoubleQuot.quotQuotMk I J = (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)).comp (Ideal.Quotient.mk I)

theorem DoubleQuot.ker_quotQuotMk {R : Type u} [CommRing R] (I J : Ideal R) : RingHom.ker (DoubleQuot.quotQuotMk I J) = I ⊔ J

The kernel of quotQuotMk

def DoubleQuot.liftSupQuotQuotMk {R : Type u} [CommRing R] (I J : Ideal R) : R ⧸ I ⊔ J →+* (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J

The ring homomorphism R/(I ⊔ J) → (R/I)/J' induced by quotQuotMk

Equations

• DoubleQuot.liftSupQuotQuotMk I J = Ideal.Quotient.lift (I ⊔ J) (DoubleQuot.quotQuotMk I J) ⋯

def DoubleQuot.quotQuotEquivQuotSup {R : Type u} [CommRing R] (I J : Ideal R) : (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J ≃+* R ⧸ I ⊔ J

quotQuotToQuotSup and liftSupQuotQuotMk are inverse isomorphisms. In the case where I ≤ J, this is the Third Isomorphism Theorem (see quotQuotEquivQuotOfLe)

Equations

• DoubleQuot.quotQuotEquivQuotSup I J = RingEquiv.ofHomInv (DoubleQuot.quotQuotToQuotSup I J) (DoubleQuot.liftSupQuotQuotMk I J) ⋯ ⋯

@[simp]

theorem DoubleQuot.quotQuotEquivQuotSup_quotQuotMk {R : Type u} [CommRing R] (I J : Ideal R) (x : R) : (DoubleQuot.quotQuotEquivQuotSup I J) ((DoubleQuot.quotQuotMk I J) x) = (Ideal.Quotient.mk (I ⊔ J)) x

@[simp]

theorem DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk {R : Type u} [CommRing R] (I J : Ideal R) (x : R) : (DoubleQuot.quotQuotEquivQuotSup I J).symm ((Ideal.Quotient.mk (I ⊔ J)) x) = (DoubleQuot.quotQuotMk I J) x

def DoubleQuot.quotQuotEquivComm {R : Type u} [CommRing R] (I J : Ideal R) : (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J ≃+* (R ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I

The obvious isomorphism (R/I)/J' → (R/J)/I'

Equations

• DoubleQuot.quotQuotEquivComm I J = ((DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯)).trans (DoubleQuot.quotQuotEquivQuotSup J I).symm

@[simp]

theorem DoubleQuot.quotQuotEquivComm_quotQuotMk {R : Type u} [CommRing R] (I J : Ideal R) (x : R) : (DoubleQuot.quotQuotEquivComm I J) ((DoubleQuot.quotQuotMk I J) x) = (DoubleQuot.quotQuotMk J I) x

@[simp]

theorem DoubleQuot.quotQuotEquivComm_comp_quotQuotMk {R : Type u} [CommRing R] (I J : Ideal R) : (↑(DoubleQuot.quotQuotEquivComm I J)).comp (DoubleQuot.quotQuotMk I J) = DoubleQuot.quotQuotMk J I

@[simp]

theorem DoubleQuot.quotQuotEquivComm_symm {R : Type u} [CommRing R] (I J : Ideal R) : (DoubleQuot.quotQuotEquivComm I J).symm = DoubleQuot.quotQuotEquivComm J I

def DoubleQuot.quotQuotEquivQuotOfLE {R : Type u} [CommRing R] {I J : Ideal R} (h : I ≤ J) : (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J ≃+* R ⧸ J

The Third Isomorphism theorem for rings. See quotQuotEquivQuotSup for a version that does not assume an inclusion of ideals.

Equations

• DoubleQuot.quotQuotEquivQuotOfLE h = (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯)

@[simp]

theorem DoubleQuot.quotQuotEquivQuotOfLE_quotQuotMk {R : Type u} [CommRing R] {I J : Ideal R} (x : R) (h : I ≤ J) : (DoubleQuot.quotQuotEquivQuotOfLE h) ((DoubleQuot.quotQuotMk I J) x) = (Ideal.Quotient.mk J) x

@[simp]

theorem DoubleQuot.quotQuotEquivQuotOfLE_symm_mk {R : Type u} [CommRing R] {I J : Ideal R} (x : R) (h : I ≤ J) : (DoubleQuot.quotQuotEquivQuotOfLE h).symm ((Ideal.Quotient.mk J) x) = (DoubleQuot.quotQuotMk I J) x

theorem DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMk {R : Type u} [CommRing R] {I J : Ideal R} (h : I ≤ J) : (↑(DoubleQuot.quotQuotEquivQuotOfLE h)).comp (DoubleQuot.quotQuotMk I J) = Ideal.Quotient.mk J

theorem DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mk {R : Type u} [CommRing R] {I J : Ideal R} (h : I ≤ J) : (↑(DoubleQuot.quotQuotEquivQuotOfLE h).symm).comp (Ideal.Quotient.mk J) = DoubleQuot.quotQuotMk I J

@[simp]

theorem DoubleQuot.quotQuotEquivComm_mk_mk {R : Type u} [CommRing R] (I J : Ideal R) (x : R) : (DoubleQuot.quotQuotEquivComm I J) ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) ((Ideal.Quotient.mk I) x)) = (algebraMap R ((R ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I)) x

@[simp]

theorem DoubleQuot.quotQuotEquivQuotSup_quot_quot_algebraMap {R : Type u} [CommSemiring R] {A : Type v} [CommRing A] [Algebra R A] (I J : Ideal A) (x : R) : (DoubleQuot.quotQuotEquivQuotSup I J) ((algebraMap R ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) = (algebraMap R (A ⧸ I ⊔ J)) x

@[simp]

theorem DoubleQuot.quotQuotEquivComm_algebraMap {R : Type u} [CommSemiring R] {A : Type v} [CommRing A] [Algebra R A] (I J : Ideal A) (x : R) : (DoubleQuot.quotQuotEquivComm I J) ((algebraMap R ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) = (algebraMap R ((A ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I)) x

def DoubleQuot.quotLeftToQuotSupₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : A ⧸ I →ₐ[R] A ⧸ I ⊔ J

The natural algebra homomorphism A / I → A / (I ⊔ J).

Equations

• DoubleQuot.quotLeftToQuotSupₐ R I J = { toRingHom := DoubleQuot.quotLeftToQuotSup I J, commutes' := ⋯ }

@[simp]

theorem DoubleQuot.quotLeftToQuotSupₐ_toRingHom (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ↑(DoubleQuot.quotLeftToQuotSupₐ R I J) = DoubleQuot.quotLeftToQuotSup I J

@[simp]

theorem DoubleQuot.coe_quotLeftToQuotSupₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ⇑(DoubleQuot.quotLeftToQuotSupₐ R I J) = ⇑(DoubleQuot.quotLeftToQuotSup I J)

def DoubleQuot.quotQuotToQuotSupₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : (A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J →ₐ[R] A ⧸ I ⊔ J

The algebra homomorphism (A / I) / J' -> A / (I ⊔ J) induced by quotQuotToQuotSup, where J' is the projection of J in A / I.

Equations

• DoubleQuot.quotQuotToQuotSupₐ R I J = { toRingHom := DoubleQuot.quotQuotToQuotSup I J, commutes' := ⋯ }

@[simp]

theorem DoubleQuot.quotQuotToQuotSupₐ_toRingHom (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ↑(DoubleQuot.quotQuotToQuotSupₐ R I J) = DoubleQuot.quotQuotToQuotSup I J

@[simp]

theorem DoubleQuot.coe_quotQuotToQuotSupₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ⇑(DoubleQuot.quotQuotToQuotSupₐ R I J) = ⇑(DoubleQuot.quotQuotToQuotSup I J)

def DoubleQuot.quotQuotMkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : A →ₐ[R] (A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J

The composition of the algebra homomorphisms A → (A / I) and (A / I) → (A / I) / J', where J' is the projection J in A / I.

Equations

• DoubleQuot.quotQuotMkₐ R I J = { toRingHom := DoubleQuot.quotQuotMk I J, commutes' := ⋯ }

@[simp]

theorem DoubleQuot.quotQuotMkₐ_toRingHom (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ↑(DoubleQuot.quotQuotMkₐ R I J) = DoubleQuot.quotQuotMk I J

@[simp]

theorem DoubleQuot.coe_quotQuotMkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ⇑(DoubleQuot.quotQuotMkₐ R I J) = ⇑(DoubleQuot.quotQuotMk I J)

def DoubleQuot.liftSupQuotQuotMkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : A ⧸ I ⊔ J →ₐ[R] (A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J

The injective algebra homomorphism A / (I ⊔ J) → (A / I) / J'induced by quot_quot_mk, where J' is the projection J in A / I.

Equations

• DoubleQuot.liftSupQuotQuotMkₐ R I J = { toRingHom := DoubleQuot.liftSupQuotQuotMk I J, commutes' := ⋯ }

@[simp]

theorem DoubleQuot.liftSupQuotQuotMkₐ_toRingHom (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ↑(DoubleQuot.liftSupQuotQuotMkₐ R I J) = DoubleQuot.liftSupQuotQuotMk I J

@[simp]

theorem DoubleQuot.coe_liftSupQuotQuotMkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ⇑(DoubleQuot.liftSupQuotQuotMkₐ R I J) = ⇑(DoubleQuot.liftSupQuotQuotMk I J)

def DoubleQuot.quotQuotEquivQuotSupₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J) ≃ₐ[R] A ⧸ I ⊔ J

quotQuotToQuotSup and liftSupQuotQuotMk are inverse isomorphisms. In the case where I ≤ J, this is the Third Isomorphism Theorem (see DoubleQuot.quotQuotEquivQuotOfLE).

Equations

• DoubleQuot.quotQuotEquivQuotSupₐ R I J = AlgEquiv.ofRingEquiv ⋯

@[simp]

theorem DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ↑(DoubleQuot.quotQuotEquivQuotSupₐ R I J) = DoubleQuot.quotQuotEquivQuotSup I J

@[simp]

theorem DoubleQuot.coe_quotQuotEquivQuotSupₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ⇑(DoubleQuot.quotQuotEquivQuotSupₐ R I J) = ⇑(DoubleQuot.quotQuotEquivQuotSup I J)

@[simp]

theorem DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ↑(DoubleQuot.quotQuotEquivQuotSupₐ R I J).symm = (DoubleQuot.quotQuotEquivQuotSup I J).symm

@[simp]

theorem DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ⇑(DoubleQuot.quotQuotEquivQuotSupₐ R I J).symm = ⇑(DoubleQuot.quotQuotEquivQuotSup I J).symm

def DoubleQuot.quotQuotEquivCommₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J) ≃ₐ[R] (A ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mkₐ R J) I

The natural algebra isomorphism (A / I) / J' → (A / J) / I', where J' (resp. I') is the projection of J in A / I (resp. I in A / J).

Equations

• DoubleQuot.quotQuotEquivCommₐ R I J = AlgEquiv.ofRingEquiv ⋯

@[simp]

theorem DoubleQuot.quotQuotEquivCommₐ_toRingEquiv (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ↑(DoubleQuot.quotQuotEquivCommₐ R I J) = DoubleQuot.quotQuotEquivComm I J

@[simp]

theorem DoubleQuot.coe_quotQuotEquivCommₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ⇑(DoubleQuot.quotQuotEquivCommₐ R I J) = ⇑(DoubleQuot.quotQuotEquivComm I J)

@[simp]

theorem DoubleQuot.quotQuotEquivComm_symmₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : (DoubleQuot.quotQuotEquivCommₐ R I J).symm = DoubleQuot.quotQuotEquivCommₐ R J I

@[simp]

theorem DoubleQuot.quotQuotEquivComm_comp_quotQuotMkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : (↑(DoubleQuot.quotQuotEquivCommₐ R I J)).comp (DoubleQuot.quotQuotMkₐ R I J) = DoubleQuot.quotQuotMkₐ R J I

def DoubleQuot.quotQuotEquivQuotOfLEₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I J : Ideal A} (h : I ≤ J) : ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J) ≃ₐ[R] A ⧸ J

The third isomorphism theorem for algebras. See quotQuotEquivQuotSupₐ for version that does not assume an inclusion of ideals.

Equations

• DoubleQuot.quotQuotEquivQuotOfLEₐ R h = AlgEquiv.ofRingEquiv ⋯

@[simp]

theorem DoubleQuot.quotQuotEquivQuotOfLEₐ_toRingEquiv (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I J : Ideal A} (h : I ≤ J) : ↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h) = DoubleQuot.quotQuotEquivQuotOfLE h

@[simp]

theorem DoubleQuot.coe_quotQuotEquivQuotOfLEₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I J : Ideal A} (h : I ≤ J) : ⇑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h) = ⇑(DoubleQuot.quotQuotEquivQuotOfLE h)

@[simp]

theorem DoubleQuot.quotQuotEquivQuotOfLEₐ_symm_toRingEquiv (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I J : Ideal A} (h : I ≤ J) : ↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h).symm = (DoubleQuot.quotQuotEquivQuotOfLE h).symm

@[simp]

theorem DoubleQuot.coe_quotQuotEquivQuotOfLEₐ_symm (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I J : Ideal A} (h : I ≤ J) : ⇑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h).symm = ⇑(DoubleQuot.quotQuotEquivQuotOfLE h).symm

@[simp]

theorem DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I J : Ideal A} (h : I ≤ J) : (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h)).comp (DoubleQuot.quotQuotMkₐ R I J) = Ideal.Quotient.mkₐ R J

@[simp]

theorem DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I J : Ideal A} (h : I ≤ J) : (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h).symm).comp (Ideal.Quotient.mkₐ R J) = DoubleQuot.quotQuotMkₐ R I J

noncomputable def Ideal.powQuotPowSuccLinearEquivMapMkPowSuccPow {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : (↥(I ^ n) ⧸ I • ⊤) ≃ₗ[R] ↥(Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n))

I ^ n ⧸ I ^ (n + 1) can be viewed as a quotient module and as ideal of R ⧸ I ^ (n + 1). This definition gives the R-linear equivalence between the two.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Ideal.powQuotPowSuccEquivMapMkPowSuccPow {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : ↥(I ^ n) ⧸ I • ⊤ ≃ ↥(Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n))

I ^ n ⧸ I ^ (n + 1) can be viewed as a quotient module and as ideal of R ⧸ I ^ (n + 1). This definition gives the equivalence between the two, instead of the R-linear equivalence, to bypass typeclass synthesis issues on complex Module goals.

Equations

• I.powQuotPowSuccEquivMapMkPowSuccPow n = ↑(I.powQuotPowSuccLinearEquivMapMkPowSuccPow n)