More operations on modules and ideals related to quotients #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
def
ring_hom.ker_lift
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
(f : R →+* S) :
R ⧸ ring_hom.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 (quotient_ker_equiv_of_right_inverse) /
is surjective (quotient_ker_equiv_of_surjective).
Equations
- f.ker_lift = ideal.quotient.lift (ring_hom.ker f) f _
@[simp]
theorem
ring_hom.ker_lift_mk
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(r : R) :
⇑(f.ker_lift) (⇑(ideal.quotient.mk (ring_hom.ker f)) r) = ⇑f r
def
ring_hom.quotient_ker_equiv_of_right_inverse
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
{f : R →+* S}
{g : S → R}
(hf : function.right_inverse g ⇑f) :
R ⧸ ring_hom.ker f ≃+* S
The first isomorphism theorem for commutative rings, computable version.
Equations
- ring_hom.quotient_ker_equiv_of_right_inverse hf = {to_fun := ⇑(f.ker_lift), inv_fun := ⇑(ideal.quotient.mk (ring_hom.ker f)) ∘ g, left_inv := _, right_inv := hf, map_mul' := _, map_add' := _}
@[simp]
theorem
ring_hom.quotient_ker_equiv_of_right_inverse.apply
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
{f : R →+* S}
{g : S → R}
(hf : function.right_inverse g ⇑f)
(x : R ⧸ ring_hom.ker f) :
⇑(ring_hom.quotient_ker_equiv_of_right_inverse hf) x = ⇑(f.ker_lift) x
@[simp]
theorem
ring_hom.quotient_ker_equiv_of_right_inverse.symm.apply
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
{f : R →+* S}
{g : S → R}
(hf : function.right_inverse g ⇑f)
(x : S) :
⇑((ring_hom.quotient_ker_equiv_of_right_inverse hf).symm) x = ⇑(ideal.quotient.mk (ring_hom.ker f)) (g x)
noncomputable
def
ring_hom.quotient_ker_equiv_of_surjective
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
{f : R →+* S}
(hf : function.surjective ⇑f) :
R ⧸ ring_hom.ker f ≃+* S
The first isomorphism theorem for commutative rings.
@[simp]
theorem
ideal.map_quotient_self
{R : Type u}
[comm_ring R]
(I : ideal R) :
ideal.map (ideal.quotient.mk I) I = ⊥
@[simp]
theorem
ideal.mk_ker
{R : Type u}
[comm_ring R]
{I : ideal R} :
ring_hom.ker (ideal.quotient.mk I) = I
theorem
ideal.map_mk_eq_bot_of_le
{R : Type u}
[comm_ring R]
{I J : ideal R}
(h : I ≤ J) :
ideal.map (ideal.quotient.mk J) I = ⊥
theorem
ideal.ker_quotient_lift
{R : Type u}
[comm_ring R]
{S : Type v}
[comm_ring S]
{I : ideal R}
(f : R →+* S)
(H : I ≤ ring_hom.ker f) :
ring_hom.ker (ideal.quotient.lift I f H) = ideal.map (ideal.quotient.mk I) (ring_hom.ker f)
@[simp]
@[simp]
theorem
ideal.mem_quotient_iff_mem_sup
{R : Type u}
[comm_ring 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}
[comm_ring 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.
theorem
ideal.comap_map_mk
{R : Type u}
[comm_ring R]
{I J : ideal R}
(h : I ≤ J) :
ideal.comap (ideal.quotient.mk I) (ideal.map (ideal.quotient.mk I) J) = J
@[protected, instance]
def
ideal.quotient.algebra
(R₁ : Type u_1)
{A : Type u_3}
[comm_semiring R₁]
[comm_ring A]
[algebra R₁ A]
{I : ideal A} :
The R₁-algebra structure on A/I for an R₁-algebra A
Equations
- ideal.quotient.algebra R₁ = {to_has_smul := {smul := has_smul.smul (submodule.quotient.has_smul' I)}, to_ring_hom := {to_fun := λ (x : R₁), ⇑(ideal.quotient.mk I) (⇑(algebra_map R₁ A) x), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
@[protected, instance]
def
ideal.quotient.is_scalar_tower
(R₁ : Type u_1)
(R₂ : Type u_2)
{A : Type u_3}
[comm_semiring R₁]
[comm_semiring R₂]
[comm_ring A]
[algebra R₁ A]
[algebra R₂ A]
[has_smul R₁ R₂]
[is_scalar_tower R₁ R₂ A]
(I : ideal A) :
is_scalar_tower R₁ R₂ (A ⧸ I)
def
ideal.quotient.mkₐ
(R₁ : Type u_1)
{A : Type u_3}
[comm_semiring R₁]
[comm_ring A]
[algebra R₁ A]
(I : ideal A) :
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 = {to_fun := λ (a : A), submodule.quotient.mk a, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
theorem
ideal.quotient.alg_hom_ext
(R₁ : Type u_1)
{A : Type u_3}
[comm_semiring R₁]
[comm_ring A]
[algebra R₁ A]
{I : ideal A}
{S : Type u_2}
[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}
[comm_semiring R₁]
[comm_ring A]
[algebra R₁ A]
(I : ideal A) :
algebra_map R₁ (A ⧸ I) = (algebra_map A (A ⧸ I)).comp (algebra_map R₁ A)
theorem
ideal.quotient.mkₐ_to_ring_hom
(R₁ : Type u_1)
{A : Type u_3}
[comm_semiring R₁]
[comm_ring A]
[algebra R₁ A]
(I : ideal A) :
(ideal.quotient.mkₐ R₁ I).to_ring_hom = ideal.quotient.mk I
@[simp]
theorem
ideal.quotient.mkₐ_eq_mk
(R₁ : Type u_1)
{A : Type u_3}
[comm_semiring R₁]
[comm_ring A]
[algebra R₁ A]
(I : ideal A) :
⇑(ideal.quotient.mkₐ R₁ I) = ⇑(ideal.quotient.mk I)
@[simp]
theorem
ideal.quotient.algebra_map_eq
{R : Type u}
[comm_ring R]
(I : ideal R) :
algebra_map R (R ⧸ I) = ideal.quotient.mk I
@[simp]
theorem
ideal.quotient.mk_comp_algebra_map
(R₁ : Type u_1)
{A : Type u_3}
[comm_semiring R₁]
[comm_ring A]
[algebra R₁ A]
(I : ideal A) :
(ideal.quotient.mk I).comp (algebra_map R₁ A) = algebra_map R₁ (A ⧸ I)
@[simp]
theorem
ideal.quotient.mk_algebra_map
(R₁ : Type u_1)
{A : Type u_3}
[comm_semiring R₁]
[comm_ring A]
[algebra R₁ A]
(I : ideal A)
(x : R₁) :
⇑(ideal.quotient.mk I) (⇑(algebra_map R₁ A) x) = ⇑(algebra_map R₁ (A ⧸ I)) x
theorem
ideal.quotient.mkₐ_surjective
(R₁ : Type u_1)
{A : Type u_3}
[comm_semiring R₁]
[comm_ring A]
[algebra R₁ A]
(I : ideal A) :
The canonical morphism A →ₐ[R₁] I.quotient is surjective.
@[simp]
theorem
ideal.quotient.mkₐ_ker
(R₁ : Type u_1)
{A : Type u_3}
[comm_semiring R₁]
[comm_ring A]
[algebra R₁ A]
(I : ideal A) :
ring_hom.ker ↑(ideal.quotient.mkₐ R₁ I) = I
The kernel of A →ₐ[R₁] I.quotient is I.
@[simp]
theorem
ideal.quotient.liftₐ_apply
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[comm_semiring R₁]
[comm_ring A]
[comm_ring B]
[algebra R₁ A]
[algebra R₁ B]
(I : ideal A)
(f : A →ₐ[R₁] B)
(hI : ∀ (a : A), a ∈ I → ⇑f a = 0)
(x : A ⧸ I) :
⇑(ideal.quotient.liftₐ I f hI) x = ⇑(ideal.quotient.lift I ↑f hI) x
theorem
ideal.ker_lift.map_smul
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[comm_semiring R₁]
[comm_ring A]
[comm_ring B]
[algebra R₁ A]
[algebra R₁ B]
(f : A →ₐ[R₁] B)
(r : R₁)
(x : A ⧸ ring_hom.ker f.to_ring_hom) :
⇑(f.to_ring_hom.ker_lift) (r • x) = r • ⇑(f.to_ring_hom.ker_lift) x
def
ideal.ker_lift_alg
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[comm_semiring R₁]
[comm_ring A]
[comm_ring B]
[algebra R₁ A]
[algebra R₁ B]
(f : A →ₐ[R₁] B) :
A ⧸ ring_hom.ker f.to_ring_hom →ₐ[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 (quotient_ker_alg_equiv_of_right_inverse) /
is surjective (quotient_ker_alg_equiv_of_surjective).
Equations
@[simp]
theorem
ideal.ker_lift_alg_mk
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[comm_semiring R₁]
[comm_ring A]
[comm_ring B]
[algebra R₁ A]
[algebra R₁ B]
(f : A →ₐ[R₁] B)
(a : A) :
⇑(ideal.ker_lift_alg f) (⇑(ideal.quotient.mk (ring_hom.ker f.to_ring_hom)) a) = ⇑f a
def
ideal.quotient_ker_alg_equiv_of_right_inverse
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[comm_semiring R₁]
[comm_ring A]
[comm_ring B]
[algebra R₁ A]
[algebra R₁ B]
{f : A →ₐ[R₁] B}
{g : B → A}
(hf : function.right_inverse g ⇑f) :
(A ⧸ ring_hom.ker f.to_ring_hom) ≃ₐ[R₁] B
The first isomorphism theorem for algebras, computable version.
Equations
- ideal.quotient_ker_alg_equiv_of_right_inverse hf = {to_fun := (ring_hom.quotient_ker_equiv_of_right_inverse _).to_fun, inv_fun := (ring_hom.quotient_ker_equiv_of_right_inverse _).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
@[simp]
theorem
ideal.quotient_ker_alg_equiv_of_right_inverse.apply
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[comm_semiring R₁]
[comm_ring A]
[comm_ring B]
[algebra R₁ A]
[algebra R₁ B]
{f : A →ₐ[R₁] B}
{g : B → A}
(hf : function.right_inverse g ⇑f)
(x : A ⧸ ring_hom.ker f.to_ring_hom) :
@[simp]
theorem
ideal.quotient_ker_alg_equiv_of_right_inverse_symm.apply
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[comm_semiring R₁]
[comm_ring A]
[comm_ring B]
[algebra R₁ A]
[algebra R₁ B]
{f : A →ₐ[R₁] B}
{g : B → A}
(hf : function.right_inverse g ⇑f)
(x : B) :
⇑((ideal.quotient_ker_alg_equiv_of_right_inverse hf).symm) x = ⇑(ideal.quotient.mkₐ R₁ (ring_hom.ker f.to_ring_hom)) (g x)
noncomputable
def
ideal.quotient_ker_alg_equiv_of_surjective
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[comm_semiring R₁]
[comm_ring A]
[comm_ring B]
[algebra R₁ A]
[algebra R₁ B]
{f : A →ₐ[R₁] B}
(hf : function.surjective ⇑f) :
(A ⧸ ring_hom.ker f.to_ring_hom) ≃ₐ[R₁] B
The first isomorphism theorem for algebras.
def
ideal.quotient_map
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
{I : ideal R}
(J : ideal S)
(f : R →+* S)
(hIJ : I ≤ ideal.comap f J) :
The ring hom R/I →+* S/J induced by a ring hom f : R →+* S with I ≤ f⁻¹(J)
Equations
- J.quotient_map f hIJ = ideal.quotient.lift I ((ideal.quotient.mk J).comp f) _
@[simp]
theorem
ideal.quotient_map_mk
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
{J : ideal R}
{I : ideal S}
{f : R →+* S}
{H : J ≤ ideal.comap f I}
{x : R} :
⇑(I.quotient_map f H) (⇑(ideal.quotient.mk J) x) = ⇑(ideal.quotient.mk I) (⇑f x)
@[simp]
theorem
ideal.quotient_map_algebra_map
{S : Type v}
[comm_ring S]
{R₁ : Type u_1}
{A : Type u_3}
[comm_semiring R₁]
[comm_ring A]
[algebra R₁ A]
{J : ideal A}
{I : ideal S}
{f : A →+* S}
{H : J ≤ ideal.comap f I}
{x : R₁} :
⇑(I.quotient_map f H) (⇑(algebra_map R₁ (A ⧸ J)) x) = ⇑(ideal.quotient.mk I) (⇑f (⇑(algebra_map R₁ A) x))
theorem
ideal.quotient_map_comp_mk
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
{J : ideal R}
{I : ideal S}
{f : R →+* S}
(H : J ≤ ideal.comap f I) :
(I.quotient_map f H).comp (ideal.quotient.mk J) = (ideal.quotient.mk I).comp f
@[simp]
theorem
ideal.quotient_equiv_mk
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
(I : ideal R)
(J : ideal S)
(f : R ≃+* S)
(hIJ : J = ideal.map ↑f I)
(x : R) :
⇑(I.quotient_equiv J f hIJ) (⇑(ideal.quotient.mk I) x) = ⇑(ideal.quotient.mk J) (⇑f x)
theorem
ideal.quotient_map_injective'
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
{J : ideal R}
{I : ideal S}
{f : R →+* S}
{H : J ≤ ideal.comap f I}
(h : ideal.comap f I ≤ J) :
function.injective ⇑(I.quotient_map f H)
H and h are kept as separate hypothesis since H is used in constructing the quotient map.
theorem
ideal.quotient_map_injective
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
{I : ideal S}
{f : R →+* S} :
If we take J = I.comap f then quotient_map is injective automatically.
theorem
ideal.quotient_map_surjective
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
{J : ideal R}
{I : ideal S}
{f : R →+* S}
{H : J ≤ ideal.comap f I}
(hf : function.surjective ⇑f) :
function.surjective ⇑(I.quotient_map f H)
theorem
ideal.comp_quotient_map_eq_of_comp_eq
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
{R' : Type u_1}
{S' : Type u_2}
[comm_ring R']
[comm_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.quotient_map g' le_rfl).comp ((ideal.comap g' I).quotient_map f le_rfl) = (I.quotient_map f' le_rfl).comp ((ideal.comap f' I).quotient_map g _)
Commutativity of a square is preserved when taking quotients by an ideal.
def
ideal.quotient_mapₐ
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[comm_semiring R₁]
[comm_ring A]
[comm_ring B]
[algebra R₁ A]
[algebra R₁ B]
{I : ideal A}
(J : ideal B)
(f : A →ₐ[R₁] B)
(hIJ : I ≤ ideal.comap f J) :
The algebra hom A/I →+* B/J induced by an algebra hom f : A →ₐ[R₁] B with I ≤ f⁻¹(J).
@[simp]
theorem
ideal.quotient_map_mkₐ
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[comm_semiring R₁]
[comm_ring A]
[comm_ring B]
[algebra R₁ A]
[algebra R₁ B]
{I : ideal A}
(J : ideal B)
(f : A →ₐ[R₁] B)
(H : I ≤ ideal.comap f J)
{x : A} :
⇑(J.quotient_mapₐ 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}
[comm_semiring R₁]
[comm_ring A]
[comm_ring B]
[algebra R₁ A]
[algebra R₁ B]
{I : ideal A}
(J : ideal B)
(f : A →ₐ[R₁] B)
(H : I ≤ ideal.comap f J) :
(J.quotient_mapₐ f H).comp (ideal.quotient.mkₐ R₁ I) = (ideal.quotient.mkₐ R₁ J).comp f
def
ideal.quotient_equiv_alg
{R₁ : Type u_1}
{A : Type u_3}
{B : Type u_4}
[comm_semiring R₁]
[comm_ring A]
[comm_ring B]
[algebra R₁ A]
[algebra R₁ B]
(I : ideal A)
(J : ideal B)
(f : A ≃ₐ[R₁] B)
(hIJ : J = ideal.map ↑f I) :
The algebra equiv A/I ≃ₐ[R] B/J induced by an algebra equiv f : A ≃ₐ[R] B,
whereJ = f(I).
@[protected, instance]
def
ideal.quotient_algebra
{R : Type u}
[comm_ring R]
{A : Type u_3}
[comm_ring A]
{I : ideal A}
[algebra R A] :
algebra (R ⧸ ideal.comap (algebra_map R A) I) (A ⧸ I)
Equations
- ideal.quotient_algebra = (I.quotient_map (algebra_map R A) ideal.quotient_algebra._proof_1).to_algebra
theorem
ideal.algebra_map_quotient_injective
{R : Type u}
[comm_ring R]
{A : Type u_3}
[comm_ring A]
{I : ideal A}
[algebra R A] :
function.injective ⇑(algebra_map (R ⧸ ideal.comap (algebra_map R A) I) (A ⧸ I))
def
ideal.quotient_equiv_alg_of_eq
(R₁ : Type u_1)
{A : Type u_3}
[comm_semiring R₁]
[comm_ring A]
[algebra R₁ A]
{I J : ideal A}
(h : I = J) :
Quotienting by equal ideals gives equivalent algebras.
Equations
@[simp]
theorem
ideal.quotient_equiv_alg_of_eq_mk
(R₁ : Type u_1)
{A : Type u_3}
[comm_semiring R₁]
[comm_ring A]
[algebra R₁ A]
{I J : ideal A}
(h : I = J)
(x : A) :
⇑(ideal.quotient_equiv_alg_of_eq R₁ h) (⇑(ideal.quotient.mk I) x) = ⇑(ideal.quotient.mk J) x
@[simp]
theorem
ideal.quotient_equiv_alg_of_eq_symm
(R₁ : Type u_1)
{A : Type u_3}
[comm_semiring R₁]
[comm_ring A]
[algebra R₁ A]
{I J : ideal A}
(h : I = J) :
The obvious ring hom R/I → R/(I ⊔ J)
Equations
- double_quot.quot_left_to_quot_sup I J = ideal.quotient.factor I (I ⊔ J) _
The kernel of quot_left_to_quot_sup
The ring homomorphism (R/I)/J' -> R/(I ⊔ J) induced by quot_left_to_quot_sup where J'
is the image of J in R/I
Equations
def
double_quot.quot_quot_mk
{R : Type u}
[comm_ring 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
- double_quot.quot_quot_mk I J = (ideal.quotient.mk (ideal.map (ideal.quotient.mk I) J)).comp (ideal.quotient.mk I)
theorem
double_quot.ker_quot_quot_mk
{R : Type u}
[comm_ring R]
(I J : ideal R) :
ring_hom.ker (double_quot.quot_quot_mk I J) = I ⊔ J
The kernel of quot_quot_mk
The ring homomorphism R/(I ⊔ J) → (R/I)/J'induced by quot_quot_mk
Equations
- double_quot.lift_sup_quot_quot_mk I J = ideal.quotient.lift (I ⊔ J) (double_quot.quot_quot_mk I J) _
quot_quot_to_quot_add and lift_sup_double_qot_mk are inverse isomorphisms. In the case where
I ≤ J, this is the Third Isomorphism Theorem (see quot_quot_equiv_quot_of_le)
Equations
@[simp]
theorem
double_quot.quot_quot_equiv_quot_sup_quot_quot_mk
{R : Type u}
[comm_ring R]
(I J : ideal R)
(x : R) :
⇑(double_quot.quot_quot_equiv_quot_sup I J) (⇑(double_quot.quot_quot_mk I J) x) = ⇑(ideal.quotient.mk (I ⊔ J)) x
@[simp]
theorem
double_quot.quot_quot_equiv_quot_sup_symm_quot_quot_mk
{R : Type u}
[comm_ring R]
(I J : ideal R)
(x : R) :
⇑((double_quot.quot_quot_equiv_quot_sup I J).symm) (⇑(ideal.quotient.mk (I ⊔ J)) x) = ⇑(double_quot.quot_quot_mk I J) x
def
double_quot.quot_quot_equiv_comm
{R : Type u}
[comm_ring 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
@[simp]
theorem
double_quot.quot_quot_equiv_comm_quot_quot_mk
{R : Type u}
[comm_ring R]
(I J : ideal R)
(x : R) :
⇑(double_quot.quot_quot_equiv_comm I J) (⇑(double_quot.quot_quot_mk I J) x) = ⇑(double_quot.quot_quot_mk J I) x
@[simp]
theorem
double_quot.quot_quot_equiv_comm_comp_quot_quot_mk
{R : Type u}
[comm_ring R]
(I J : ideal R) :
@[simp]
The Third Isomorphism theorem for rings. See quot_quot_equiv_quot_sup for a version
that does not assume an inclusion of ideals.
Equations
@[simp]
theorem
double_quot.quot_quot_equiv_quot_of_le_quot_quot_mk
{R : Type u}
[comm_ring R]
{I J : ideal R}
(x : R)
(h : I ≤ J) :
⇑(double_quot.quot_quot_equiv_quot_of_le h) (⇑(double_quot.quot_quot_mk I J) x) = ⇑(ideal.quotient.mk J) x
@[simp]
theorem
double_quot.quot_quot_equiv_quot_of_le_symm_mk
{R : Type u}
[comm_ring R]
{I J : ideal R}
(x : R)
(h : I ≤ J) :
⇑((double_quot.quot_quot_equiv_quot_of_le h).symm) (⇑(ideal.quotient.mk J) x) = ⇑(double_quot.quot_quot_mk I J) x
theorem
double_quot.quot_quot_equiv_quot_of_le_comp_quot_quot_mk
{R : Type u}
[comm_ring R]
{I J : ideal R}
(h : I ≤ J) :
theorem
double_quot.quot_quot_equiv_quot_of_le_symm_comp_mk
{R : Type u}
[comm_ring R]
{I J : ideal R}
(h : I ≤ J) :
@[simp]
theorem
double_quot.quot_quot_equiv_comm_mk_mk
{R : Type u}
[comm_ring R]
(I J : ideal R)
(x : R) :
⇑(double_quot.quot_quot_equiv_comm I J) (⇑(ideal.quotient.mk (ideal.map (ideal.quotient.mk I) J)) (⇑(ideal.quotient.mk I) x)) = ⇑(algebra_map R ((R ⧸ J) ⧸ ideal.map (ideal.quotient.mk J) I)) x
@[simp]
theorem
double_quot.quot_quot_equiv_quot_sup_quot_quot_algebra_map
{R : Type u}
[comm_semiring R]
{A : Type v}
[comm_ring A]
[algebra R A]
(I J : ideal A)
(x : R) :
⇑(double_quot.quot_quot_equiv_quot_sup I J) (⇑(algebra_map R ((A ⧸ I) ⧸ ideal.map (ideal.quotient.mk I) J)) x) = ⇑(algebra_map R (A ⧸ I ⊔ J)) x
@[simp]
theorem
double_quot.quot_quot_equiv_comm_algebra_map
{R : Type u}
[comm_semiring R]
{A : Type v}
[comm_ring A]
[algebra R A]
(I J : ideal A)
(x : R) :
⇑(double_quot.quot_quot_equiv_comm I J) (⇑(algebra_map R ((A ⧸ I) ⧸ ideal.map (ideal.quotient.mk I) J)) x) = ⇑(algebra_map R ((A ⧸ J) ⧸ ideal.map (ideal.quotient.mk J) I)) x
def
double_quot.quot_left_to_quot_supₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
The natural algebra homomorphism A / I → A / (I ⊔ J).
@[simp]
theorem
double_quot.quot_left_to_quot_supₐ_to_ring_hom
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
@[simp]
theorem
double_quot.coe_quot_left_to_quot_supₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
def
double_quot.quot_quot_to_quot_supₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
The algebra homomorphism (A / I) / J' -> A / (I ⊔ J) induced byquot_left_to_quot_sup, whereJ'is the projection ofJinA / I`.
@[simp]
theorem
double_quot.quot_quot_to_quot_supₐ_to_ring_hom
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
@[simp]
theorem
double_quot.coe_quot_quot_to_quot_supₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
def
double_quot.quot_quot_mkₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring 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.
@[simp]
theorem
double_quot.quot_quot_mkₐ_to_ring_hom
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
@[simp]
theorem
double_quot.coe_quot_quot_mkₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
⇑(double_quot.quot_quot_mkₐ R I J) = ⇑(double_quot.quot_quot_mk I J)
def
double_quot.lift_sup_quot_quot_mkₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring 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.
@[simp]
theorem
double_quot.lift_sup_quot_quot_mkₐ_to_ring_hom
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
@[simp]
theorem
double_quot.coe_lift_sup_quot_quot_mkₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
def
double_quot.quot_quot_equiv_quot_supₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
quot_quot_to_quot_add and lift_sup_quot_quot_mk are inverse isomorphisms. In the case where
I ≤ J, this is the Third Isomorphism Theorem (see quot_quot_equiv_quot_of_le).
Equations
@[simp]
theorem
double_quot.quot_quot_equiv_quot_supₐ_to_ring_equiv
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
@[simp]
theorem
double_quot.coe_quot_quot_equiv_quot_supₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
@[simp]
theorem
double_quot.quot_quot_equiv_quot_supₐ_symm_to_ring_equiv
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
@[simp]
theorem
double_quot.coe_quot_quot_equiv_quot_supₐ_symm
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
⇑((double_quot.quot_quot_equiv_quot_supₐ R I J).symm) = ⇑((double_quot.quot_quot_equiv_quot_sup I J).symm)
def
double_quot.quot_quot_equiv_commₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring 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
double_quot.quot_quot_equiv_commₐ_to_ring_equiv
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
@[simp]
theorem
double_quot.coe_quot_quot_equiv_commₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
@[simp]
theorem
double_quot.quot_quot_equiv_comm_symmₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
@[simp]
theorem
double_quot.quot_quot_equiv_comm_comp_quot_quot_mkₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
(I J : ideal A) :
↑(double_quot.quot_quot_equiv_commₐ R I J).comp (double_quot.quot_quot_mkₐ R I J) = double_quot.quot_quot_mkₐ R J I
def
double_quot.quot_quot_equiv_quot_of_leₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
{I J : ideal A}
(h : I ≤ J) :
The third isomoprhism theorem for rings. See quot_quot_equiv_quot_sup for version
that does not assume an inclusion of ideals.
Equations
@[simp]
theorem
double_quot.quot_quot_equiv_quot_of_leₐ_to_ring_equiv
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
{I J : ideal A}
(h : I ≤ J) :
@[simp]
theorem
double_quot.coe_quot_quot_equiv_quot_of_leₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
{I J : ideal A}
(h : I ≤ J) :
@[simp]
theorem
double_quot.quot_quot_equiv_quot_of_leₐ_symm_to_ring_equiv
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
{I J : ideal A}
(h : I ≤ J) :
@[simp]
theorem
double_quot.coe_quot_quot_equiv_quot_of_leₐ_symm
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
{I J : ideal A}
(h : I ≤ J) :
@[simp]
theorem
double_quot.quot_quot_equiv_quot_of_le_comp_quot_quot_mkₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
{I J : ideal A}
(h : I ≤ J) :
↑(double_quot.quot_quot_equiv_quot_of_leₐ R h).comp (double_quot.quot_quot_mkₐ R I J) = ideal.quotient.mkₐ R J
@[simp]
theorem
double_quot.quot_quot_equiv_quot_of_le_symm_comp_mkₐ
(R : Type u)
{A : Type u_1}
[comm_semiring R]
[comm_ring A]
[algebra R A]
{I J : ideal A}
(h : I ≤ J) :
↑((double_quot.quot_quot_equiv_quot_of_leₐ R h).symm).comp (ideal.quotient.mkₐ R J) = double_quot.quot_quot_mkₐ R I J