Documentation

Mathlib.RingTheory.Ideal.Quotient.Basic

Ideal quotients #

This file defines ideal quotients as a special case of submodule quotients and proves some basic results about these quotients.

See Algebra.RingQuot for quotients of non-commutative rings.

Main definitions #

theorem Ideal.Quotient.isScalarTower_right {R : Type u} [CommRing R] {I : Ideal R} {α : Type u_1} [SMul α R] [IsScalarTower α R R] :
IsScalarTower α (R I) (R I)
theorem Ideal.Quotient.smulCommClass {R : Type u} [CommRing R] {I : Ideal R} {α : Type u_1} [SMul α R] [IsScalarTower α R R] [SMulCommClass α R R] :
SMulCommClass α (R I) (R I)
theorem Ideal.Quotient.smulCommClass' {R : Type u} [CommRing R] {I : Ideal R} {α : Type u_1} [SMul α R] [IsScalarTower α R R] [SMulCommClass R α R] :
SMulCommClass (R I) α (R I)
@[simp]
theorem Ideal.Quotient.zero_eq_one_iff {R : Type u} [CommRing R] {I : Ideal R} :
0 = 1 I =
theorem Ideal.Quotient.nontrivial {R : Type u} [CommRing R] {I : Ideal R} (hI : I ) :
Equations
  • Ideal.Quotient.instUniqueQuotientTop = { default := 0, uniq := }
theorem Ideal.Quotient.noZeroDivisors {R : Type u} [CommRing R] (I : Ideal R) [hI : I.IsPrime] :
theorem Ideal.Quotient.isDomain {R : Type u} [CommRing R] (I : Ideal R) [hI : I.IsPrime] :
theorem Ideal.Quotient.isDomain_iff_prime {R : Type u} [CommRing R] (I : Ideal R) :
IsDomain (R I) I.IsPrime
theorem Ideal.Quotient.exists_inv {R : Type u} [CommRing R] {I : Ideal R} [hI : I.IsMaximal] {a : R I} :
a 0∃ (b : R I), a * b = 1
@[reducible, inline]
noncomputable abbrev Ideal.Quotient.groupWithZero {R : Type u} [CommRing R] (I : Ideal R) [hI : I.IsMaximal] :

The quotient by a maximal ideal is a group with zero. This is a def rather than instance, since users will have computable inverses in some applications.

See note [reducible non-instances].

Equations
Instances For
    @[reducible, inline]
    noncomputable abbrev Ideal.Quotient.field {R : Type u} [CommRing R] (I : Ideal R) [I.IsMaximal] :
    Field (R I)

    The quotient by a maximal ideal is a field. This is a def rather than instance, since users will have computable inverses (and qsmul, ratCast) in some applications.

    See note [reducible non-instances].

    Equations
    Instances For
      theorem Ideal.Quotient.maximal_of_isField {R : Type u} [CommRing R] (I : Ideal R) (hqf : IsField (R I)) :
      I.IsMaximal

      If the quotient by an ideal is a field, then the ideal is maximal.

      theorem Ideal.Quotient.maximal_ideal_iff_isField_quotient {R : Type u} [CommRing R] (I : Ideal R) :
      I.IsMaximal IsField (R I)

      The quotient of a ring by an ideal is a field iff the ideal is maximal.

      instance Ideal.modulePi {R : Type u} [CommRing R] (I : Ideal R) (ι : Type v) :
      Module (R I) ((ιR) I.pi ι)

      R^n/I^n is a R/I-module.

      Equations
      noncomputable def Ideal.piQuotEquiv {R : Type u} [CommRing R] (I : Ideal R) (ι : Type v) :
      ((ιR) I.pi ι) ≃ₗ[R I] ιR I

      R^n/I^n is isomorphic to (R/I)^n as an R/I-module.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem Ideal.map_pi {R : Type u} [CommRing R] (I : Ideal R) {ι : Type u_1} [Finite ι] {ι' : Type w} (x : ιR) (hi : ∀ (i : ι), x i I) (f : (ιR) →ₗ[R] ι'R) (i : ι') :
        f x i I

        If f : R^n → R^m is an R-linear map and I ⊆ R is an ideal, then the image of I^n is contained in I^m.

        theorem Ideal.univ_eq_iUnion_image_add {R : Type u_1} [Ring R] (I : Ideal R) :
        Set.univ = ⋃ (x : R I), Quotient.out x +ᵥ I

        A ring is made up of a disjoint union of cosets of an ideal.

        theorem Finite.of_finite_quot_finite_ideal {R : Type u_1} [Ring R] {I : Ideal R} [hI : Finite I] [h : Finite (R I)] :