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 alsoZMod.prodEquivPiinData.ZMod.Quotientfor elementary versions aboutZMod).
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 ⋯
theorem
RingHom.lift_injective_of_ker_le_ideal
{R : Type u}
{S : Type v}
[Ring R]
[Semiring S]
(I : Ideal R)
[I.IsTwoSided]
{f : R →+* S}
(H : ∀ a ∈ I, f a = 0)
(hI : ker f ≤ I)
:
Function.Injective ⇑(Ideal.Quotient.lift I f H)
def
RingHom.quotientKerEquivOfRightInverse
{R : Type u}
{S : Type v}
[Ring R]
[Semiring S]
{f : R →+* S}
{g : S → R}
(hf : Function.RightInverse g ⇑f)
:
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}
[Ring R]
[Semiring S]
{f : R →+* S}
{g : S → R}
(hf : Function.RightInverse g ⇑f)
(x : R ⧸ ker f)
:
@[simp]
theorem
RingHom.quotientKerEquivOfRightInverse.Symm.apply
{R : Type u}
{S : Type v}
[Ring R]
[Semiring S]
{f : R →+* S}
{g : S → R}
(hf : Function.RightInverse g ⇑f)
(x : S)
:
The quotient of a ring by he zero ideal is isomorphic to the ring itself.
Equations
noncomputable def
RingHom.quotientKerEquivOfSurjective
{R : Type u}
{S : Type v}
[Ring R]
[Semiring S]
{f : R →+* S}
(hf : Function.Surjective ⇑f)
:
The first isomorphism theorem for commutative rings, surjective case.
noncomputable def
RingHom.quotientKerEquivRangeS
{R : Type u}
{S : Type v}
[Ring R]
[Semiring S]
(f : R →+* S)
:
The first isomorphism theorem for commutative rings (RingHom.rangeS version).
Equations
noncomputable def
RingHom.quotientKerEquivRange
{R : Type u}
[Ring R]
{S : Type v}
[Ring S]
(f : R →+* S)
:
The first isomorphism theorem for commutative rings (RingHom.range version).
Equations
@[simp]
@[simp]
theorem
Ideal.map_mk_eq_bot_of_le
{R : Type u}
[Ring R]
{I J : Ideal R}
[J.IsTwoSided]
(h : I ≤ J)
:
theorem
Ideal.ker_quotient_lift
{R : Type u}
{S : Type v}
[Ring R]
[Semiring S]
{I : Ideal R}
[I.IsTwoSided]
(f : R →+* S)
(H : I ≤ RingHom.ker f)
:
theorem
Ideal.injective_lift_iff
{R : Type u}
{S : Type v}
[Ring R]
[Semiring S]
{I : Ideal R}
[I.IsTwoSided]
{f : R →+* S}
(H : ∀ a ∈ I, f a = 0)
:
theorem
Ideal.ker_Pi_Quotient_mk
{R : Type u}
[Ring R]
{ι : Type u_1}
(I : ι → Ideal R)
[∀ (i : ι), (I i).IsTwoSided]
:
@[simp]
@[simp]
theorem
Ideal.mem_quotient_iff_mem_sup
{R : Type u}
[Ring R]
{I J : Ideal R}
[I.IsTwoSided]
{x : R}
:
See also Ideal.mem_quotient_iff_mem in case I ≤ J.
theorem
Ideal.mem_quotient_iff_mem
{R : Type u}
[Ring R]
{I J : Ideal R}
[I.IsTwoSided]
(hIJ : I ≤ J)
{x : R}
:
See also Ideal.mem_quotient_iff_mem_sup if the assumption I ≤ J is not available.
def
Ideal.quotientInfToPiQuotient
{R : Type u}
[Ring R]
{ι : Type u_1}
(I : ι → Ideal R)
[∀ (i : ι), (I i).IsTwoSided]
:
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}
[Ring R]
{ι : Type u_1}
(I : ι → Ideal R)
[∀ (i : ι), (I i).IsTwoSided]
(x : R)
:
(quotientInfToPiQuotient I) ((Quotient.mk (⨅ (i : ι), I i)) x) = fun (i : ι) => (Quotient.mk (I i)) x
theorem
Ideal.quotientInfToPiQuotient_mk'
{R : Type u}
[Ring R]
{ι : Type u_1}
(I : ι → Ideal R)
[∀ (i : ι), (I i).IsTwoSided]
(x : R)
(i : ι)
:
theorem
Ideal.quotientInfToPiQuotient_inj
{R : Type u}
[Ring R]
{ι : Type u_1}
(I : ι → Ideal R)
[∀ (i : ι), (I i).IsTwoSided]
:
theorem
Ideal.quotientInfToPiQuotient_surj
{R : Type u_2}
[CommRing R]
{ι : Type u_3}
[Finite ι]
{I : ι → Ideal R}
(hI : Pairwise (Function.onFun IsCoprime I))
:
noncomputable def
Ideal.quotientInfRingEquivPiQuotient
{R : Type u_2}
[CommRing R]
{ι : Type u_3}
[Finite ι]
(f : ι → Ideal R)
(hf : Pairwise (Function.onFun IsCoprime f))
:
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 : ι), (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)
:
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_2}
[CommRing R]
(I J : Ideal R)
(coprime : IsCoprime I 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.fst_comp_quotientInfEquivQuotientProd
{R : Type u_2}
[CommRing R]
(I J : Ideal R)
(coprime : IsCoprime I J)
:
@[simp]
theorem
Ideal.snd_comp_quotientInfEquivQuotientProd
{R : Type u_2}
[CommRing R]
(I J : Ideal R)
(coprime : IsCoprime I J)
:
noncomputable def
Ideal.quotientMulEquivQuotientProd
{R : Type u_2}
[CommRing R]
(I J : Ideal R)
(coprime : IsCoprime I J)
:
Chinese remainder theorem, specialized to two ideals.
Equations
- I.quotientMulEquivQuotientProd J coprime = (Ideal.quotEquivOfEq ⋯).trans (I.quotientInfEquivQuotientProd J coprime)
@[simp]
theorem
Ideal.fst_comp_quotientMulEquivQuotientProd
{R : Type u_2}
[CommRing R]
(I J : Ideal R)
(coprime : IsCoprime I J)
:
@[simp]
theorem
Ideal.snd_comp_quotientMulEquivQuotientProd
{R : Type u_2}
[CommRing R]
(I J : Ideal R)
(coprime : IsCoprime I J)
:
instance
Ideal.Quotient.algebra
(R₁ : Type u_1)
{A : Type u_3}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
{I : Ideal A}
[I.IsTwoSided]
:
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.instAlgebraQuotient
(R₁ : Type u_1)
[CommSemiring R₁]
{A : Type u_5}
[CommRing A]
[Algebra R₁ A]
(I : Ideal A)
:
Equations
instance
Ideal.Quotient.isScalarTower
(R₁ : Type u_1)
(R₂ : Type u_2)
{A : Type u_3}
[CommSemiring R₁]
[CommSemiring R₂]
[Ring 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₁]
[Ring A]
[Algebra R₁ A]
(I : Ideal A)
[I.IsTwoSided]
:
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.alg_map_eq
(R₁ : Type u_1)
[CommSemiring R₁]
{A : Type u_5}
[CommRing A]
[Algebra R₁ A]
(I : Ideal A)
:
theorem
Ideal.Quotient.mkₐ_toRingHom
(R₁ : Type u_1)
{A : Type u_3}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
(I : Ideal A)
[I.IsTwoSided]
:
@[simp]
theorem
Ideal.Quotient.mkₐ_eq_mk
(R₁ : Type u_1)
{A : Type u_3}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
(I : Ideal A)
[I.IsTwoSided]
:
@[simp]
@[simp]
theorem
Ideal.Quotient.mk_comp_algebraMap
(R₁ : Type u_1)
{A : Type u_3}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
(I : Ideal A)
[I.IsTwoSided]
:
@[simp]
theorem
Ideal.Quotient.mk_algebraMap
(R₁ : Type u_1)
{A : Type u_3}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
(I : Ideal A)
[I.IsTwoSided]
(x : R₁)
:
theorem
Ideal.Quotient.mkₐ_surjective
(R₁ : Type u_1)
{A : Type u_3}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
(I : Ideal A)
[I.IsTwoSided]
:
Function.Surjective ⇑(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₁]
[Ring A]
[Algebra R₁ A]
(I : Ideal A)
[I.IsTwoSided]
:
The kernel of A →ₐ[R₁] I.quotient is I.
theorem
Ideal.Quotient.mk_bijective_iff_eq_bot
{A : Type u_3}
[Ring A]
(I : Ideal A)
[I.IsTwoSided]
:
def
Ideal.Quotient.liftₐ
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
[Semiring B]
[Algebra R₁ B]
(I : Ideal A)
[I.IsTwoSided]
(f : A →ₐ[R₁] B)
(hI : ∀ a ∈ I, f a = 0)
:
Ideal.quotient.lift as an AlgHom.
Equations
- Ideal.Quotient.liftₐ I f hI = { toRingHom := Ideal.Quotient.lift I (↑f) hI, commutes' := ⋯ }
def
Ideal.kerLiftAlg
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
[Semiring B]
[Algebra R₁ B]
(f : A →ₐ[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 ⋯
def
Ideal.quotientKerAlgEquivOfRightInverse
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
[Semiring B]
[Algebra R₁ B]
{f : A →ₐ[R₁] B}
{g : B → A}
(hf : Function.RightInverse g ⇑f)
:
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₁]
[Ring 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)
:
@[simp]
theorem
Ideal.quotientKerAlgEquivOfRightInverse_symm_apply
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
[Semiring B]
[Algebra R₁ B]
{f : A →ₐ[R₁] B}
{g : B → A}
(hf : Function.RightInverse g ⇑f)
(a✝ : B)
:
noncomputable def
Ideal.quotientKerAlgEquivOfSurjective
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
[Semiring B]
[Algebra R₁ B]
{f : A →ₐ[R₁] B}
(hf : Function.Surjective ⇑f)
:
The first isomorphism theorem for algebras.
@[simp]
theorem
Ideal.quotientKerAlgEquivOfSurjective_apply
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
[Semiring B]
[Algebra R₁ B]
{f : A →ₐ[R₁] B}
(hf : Function.Surjective ⇑f)
(a : A ⧸ RingHom.ker f.toRingHom)
:
@[simp]
theorem
Ideal.quotientKerAlgEquivOfSurjective_symm_apply
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
[Semiring B]
[Algebra R₁ B]
{f : A →ₐ[R₁] B}
(hf : Function.Surjective ⇑f)
(a✝ : B)
:
(quotientKerAlgEquivOfSurjective hf).symm a✝ = (Quotient.mk (RingHom.ker ↑f)) (Classical.choose ⋯ a✝)
def
Ideal.quotientMap
{R : Type u}
[Ring R]
{S : Type v}
[Ring S]
{I : Ideal R}
(J : Ideal S)
[I.IsTwoSided]
[J.IsTwoSided]
(f : R →+* S)
(hIJ : I ≤ comap f 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}
[Ring R]
{S : Type v}
[Ring S]
{J : Ideal R}
{I : Ideal S}
[I.IsTwoSided]
[J.IsTwoSided]
{f : R →+* S}
{H : J ≤ comap f I}
{x : R}
:
@[simp]
theorem
Ideal.quotientMap_algebraMap
{R₁ : Type u_1}
{A : Type u_3}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
{S : Type v}
[Ring S]
{J : Ideal A}
{I : Ideal S}
[I.IsTwoSided]
[J.IsTwoSided]
{f : A →+* S}
{H : J ≤ comap f I}
{x : R₁}
:
theorem
Ideal.quotientMap_comp_mk
{R : Type u}
[Ring R]
{S : Type v}
[Ring S]
{J : Ideal R}
{I : Ideal S}
[I.IsTwoSided]
[J.IsTwoSided]
{f : R →+* S}
(H : J ≤ comap f I)
:
theorem
Ideal.ker_quotientMap_mk
{R : Type u}
[Ring R]
{I J : Ideal R}
[I.IsTwoSided]
[J.IsTwoSided]
:
def
Ideal.quotientEquiv
{R : Type u}
[Ring R]
{S : Type v}
[Ring S]
(I : Ideal R)
(J : Ideal S)
[I.IsTwoSided]
[J.IsTwoSided]
(f : R ≃+* S)
(hIJ : J = map (↑f) I)
:
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}
[Ring R]
{S : Type v}
[Ring S]
(I : Ideal R)
(J : Ideal S)
[I.IsTwoSided]
[J.IsTwoSided]
(f : R ≃+* S)
(hIJ : J = map (↑f) I)
(a✝ : R ⧸ I)
:
@[simp]
theorem
Ideal.quotientEquiv_symm_apply
{R : Type u}
[Ring R]
{S : Type v}
[Ring S]
(I : Ideal R)
(J : Ideal S)
[I.IsTwoSided]
[J.IsTwoSided]
(f : R ≃+* S)
(hIJ : J = map (↑f) I)
(a : S ⧸ J)
:
theorem
Ideal.quotientEquiv_mk
{R : Type u}
[Ring R]
{S : Type v}
[Ring S]
(I : Ideal R)
(J : Ideal S)
[I.IsTwoSided]
[J.IsTwoSided]
(f : R ≃+* S)
(hIJ : J = map (↑f) I)
(x : R)
:
@[simp]
theorem
Ideal.quotientEquiv_symm_mk
{R : Type u}
[Ring R]
{S : Type v}
[Ring S]
(I : Ideal R)
(J : Ideal S)
[I.IsTwoSided]
[J.IsTwoSided]
(f : R ≃+* S)
(hIJ : J = map (↑f) I)
(x : S)
:
theorem
Ideal.quotientMap_injective'
{R : Type u}
[Ring R]
{S : Type v}
[Ring S]
{J : Ideal R}
{I : Ideal S}
[I.IsTwoSided]
[J.IsTwoSided]
{f : R →+* S}
{H : J ≤ comap f I}
(h : comap f I ≤ J)
:
Function.Injective ⇑(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}
[Ring R]
{S : Type v}
[Ring S]
{I : Ideal S}
{f : R →+* S}
[I.IsTwoSided]
:
Function.Injective ⇑(quotientMap I f ⋯)
If we take J = I.comap f then quotientMap is injective automatically.
theorem
Ideal.quotientMap_surjective
{R : Type u}
[Ring R]
{S : Type v}
[Ring S]
{J : Ideal R}
{I : Ideal S}
[I.IsTwoSided]
[J.IsTwoSided]
{f : R →+* S}
{H : J ≤ comap f I}
(hf : Function.Surjective ⇑f)
:
Function.Surjective ⇑(quotientMap I f H)
theorem
Ideal.comp_quotientMap_eq_of_comp_eq
{R : Type u}
[Ring R]
{S : Type v}
[Ring S]
{R' : Type u_5}
{S' : Type u_6}
[Ring R']
[Ring S']
{f : R →+* S}
{f' : R' →+* S'}
{g : R →+* R'}
{g' : S →+* S'}
(hfg : f'.comp g = g'.comp f)
(I : Ideal S')
[I.IsTwoSided]
:
let leq := ⋯;
(quotientMap I g' ⋯).comp (quotientMap (comap g' I) f ⋯) = (quotientMap I f' ⋯).comp (quotientMap (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₁]
[Ring A]
[Algebra R₁ A]
[Ring B]
[Algebra R₁ B]
{I : Ideal A}
(J : Ideal B)
[I.IsTwoSided]
[J.IsTwoSided]
(f : A →ₐ[R₁] B)
(hIJ : I ≤ comap f 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₁]
[Ring A]
[Algebra R₁ A]
[Ring B]
[Algebra R₁ B]
{I : Ideal A}
(J : Ideal B)
[I.IsTwoSided]
[J.IsTwoSided]
(f : A →ₐ[R₁] B)
(H : I ≤ comap f J)
{x : A}
:
theorem
Ideal.quotient_map_comp_mkₐ
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
[Ring B]
[Algebra R₁ B]
{I : Ideal A}
(J : Ideal B)
[I.IsTwoSided]
[J.IsTwoSided]
(f : A →ₐ[R₁] B)
(H : I ≤ comap f J)
:
def
Ideal.quotientEquivAlg
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
[Ring B]
[Algebra R₁ B]
(I : Ideal A)
(J : Ideal B)
[I.IsTwoSided]
[J.IsTwoSided]
(f : A ≃ₐ[R₁] B)
(hIJ : J = map (↑f) I)
:
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
{A : Type u_3}
[Ring A]
{R : Type u_5}
[CommRing R]
[Algebra R A]
{p : Ideal R}
{P : Ideal A}
[P.IsTwoSided]
(h : p ≤ comap (algebraMap R 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
{A : Type u_3}
[Ring A]
{R : Type u_5}
[CommRing R]
{I : Ideal A}
[I.IsTwoSided]
[Algebra R A]
:
Algebra (R ⧸ comap (algebraMap R A) I) (A ⧸ I)
theorem
Ideal.algebraMap_quotient_injective
{A : Type u_3}
[Ring A]
{R : Type u_5}
[CommRing R]
{I : Ideal A}
[I.IsTwoSided]
[Algebra R A]
:
Function.Injective ⇑(algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I))
def
Ideal.quotientEquivAlgOfEq
(R₁ : Type u_1)
{A : Type u_3}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
{I J : Ideal A}
[I.IsTwoSided]
[J.IsTwoSided]
(h : I = 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₁]
[Ring A]
[Algebra R₁ A]
{I J : Ideal A}
[I.IsTwoSided]
[J.IsTwoSided]
(h : I = J)
(x : A)
:
@[simp]
theorem
Ideal.quotientEquivAlgOfEq_symm
(R₁ : Type u_1)
{A : Type u_3}
[CommSemiring R₁]
[Ring A]
[Algebra R₁ A]
{I J : Ideal A}
[I.IsTwoSided]
[J.IsTwoSided]
(h : I = J)
:
noncomputable def
Ideal.quotientKerEquivRange
{R : Type u_5}
{A : Type u_6}
{B : Type u_7}
[CommSemiring R]
[Ring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
(f : A →ₐ[R] B)
:
The first isomorphism theorem for commutative algebras (AlgHom.range version).
Equations
The obvious ring hom R/I → R/(I ⊔ J)
Equations
The kernel of quotLeftToQuotSup
The ring homomorphism (R/I)/J' -> R/(I ⊔ J) induced by quotLeftToQuotSup where J'
is the image of J in R/I
Equations
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)
The kernel of quotQuotMk
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) ⋯
quotQuotToQuotSup and liftSupQuotQuotMk are inverse isomorphisms. In the case where
I ≤ J, this is the Third Isomorphism Theorem (see quotQuotEquivQuotOfLe).
Equations
@[simp]
theorem
DoubleQuot.quotQuotEquivQuotSup_quotQuotMk
{R : Type u}
[CommRing R]
(I J : Ideal R)
(x : R)
:
@[simp]
theorem
DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk
{R : Type u}
[CommRing R]
(I J : Ideal R)
(x : R)
:
The obvious isomorphism (R/I)/J' → (R/J)/I'
Equations
@[simp]
@[simp]
@[simp]
The Third Isomorphism theorem for rings. See quotQuotEquivQuotSup for a version
that does not assume an inclusion of ideals.
Equations
@[simp]
theorem
DoubleQuot.quotQuotEquivQuotOfLE_quotQuotMk
{R : Type u}
[CommRing R]
{I J : Ideal R}
(x : R)
(h : I ≤ J)
:
@[simp]
theorem
DoubleQuot.quotQuotEquivQuotOfLE_symm_mk
{R : Type u}
[CommRing R]
{I J : Ideal R}
(x : R)
(h : I ≤ J)
:
theorem
DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMk
{R : Type u}
[CommRing R]
{I J : Ideal R}
(h : I ≤ J)
:
theorem
DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mk
{R : Type u}
[CommRing R]
{I J : Ideal R}
(h : I ≤ J)
:
@[simp]
theorem
DoubleQuot.quotQuotEquivComm_mk_mk
{R : Type u}
[CommRing R]
(I J : Ideal R)
(x : R)
:
(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)
:
(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)
:
(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)
:
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)
:
@[simp]
theorem
DoubleQuot.coe_quotLeftToQuotSupₐ
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
def
DoubleQuot.quotQuotToQuotSupₐ
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
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)
:
@[simp]
theorem
DoubleQuot.coe_quotQuotToQuotSupₐ
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
def
DoubleQuot.quotQuotMkₐ
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
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)
:
@[simp]
theorem
DoubleQuot.coe_quotQuotMkₐ
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
def
DoubleQuot.liftSupQuotQuotMkₐ
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
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)
:
@[simp]
theorem
DoubleQuot.coe_liftSupQuotQuotMkₐ
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
def
DoubleQuot.quotQuotEquivQuotSupₐ
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
quotQuotToQuotSup and liftSupQuotQuotMk are inverse isomorphisms. In the case where
I ≤ J, this is the Third Isomorphism Theorem (see DoubleQuot.quotQuotEquivQuotOfLE).
Equations
@[simp]
theorem
DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
@[simp]
theorem
DoubleQuot.coe_quotQuotEquivQuotSupₐ
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
@[simp]
theorem
DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
@[simp]
theorem
DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
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
@[simp]
theorem
DoubleQuot.quotQuotEquivCommₐ_toRingEquiv
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
@[simp]
theorem
DoubleQuot.coe_quotQuotEquivCommₐ
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
@[simp]
theorem
DoubleQuot.quotQuotEquivComm_symmₐ
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
@[simp]
theorem
DoubleQuot.quotQuotEquivComm_comp_quotQuotMkₐ
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
(I J : Ideal A)
:
def
DoubleQuot.quotQuotEquivQuotOfLEₐ
(R : Type u)
{A : Type u_1}
[CommSemiring R]
[CommRing A]
[Algebra R A]
{I J : Ideal A}
(h : I ≤ J)
:
The third isomorphism theorem for algebras. See quotQuotEquivQuotSupₐ for version
that does not assume an inclusion of ideals.
Equations
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
noncomputable def
Ideal.powQuotPowSuccLinearEquivMapMkPowSuccPow
{R : Type u_1}
[CommRing R]
(I : Ideal R)
(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 ^ (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.