PhysLean Documentation

Mathlib.RingTheory.Ideal.Quotient.PowTransition

The quotient map from R ⧸ I ^ m to R ⧸ I ^ n where m ≥ n #

In this file we define the canonical quotient linear map from M ⧸ I ^ m • ⊤ to M ⧸ I ^ n • ⊤ and canonical quotient ring map from R ⧸ I ^ m to R ⧸ I ^ n. These definitions will be used in theorems related to IsAdicComplete to find a lift element from compatible sequences in the quotients. We also include results about the relation between quotients of submodules and quotients of ideals here.

Main definitions #

Main results #

source
theorem Ideal.Quotient.factor_ker {R : Type u_1} [Ring R] {I J : Ideal R} (H : I ≤ J) [I.IsTwoSided] [J.IsTwoSided] :
RingHom.ker (factor H) = map (mk I) J
source
theorem Ideal.map_mk_comap_factor {R : Type u_1} [Ring R] {I J K : Ideal R} [J.IsTwoSided] [K.IsTwoSided] (hIJ : J ≤ I) (hJK : K ≤ J) :
comap (Quotient.factor hJK) (map (Quotient.mk J) I) = map (Quotient.mk K) I
source
@[simp]
theorem Submodule.mapQ_eq_factor {R : Type u_1} [Ring R] {I J : Ideal R} (h : I ≤ J) (x : R ⧸ I) :
(mapQ I J LinearMap.id h) x = (factor h) x
source
theorem Submodule.pow_smul_top_le {R : Type u_1} [Ring R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] {m n : ℕ} (h : m ≤ n) :
I ^ n • ⊤ ≤ I ^ m • ⊤
source
@[reducible, inline]
abbrev Submodule.factorPow {R : Type u_1} [Ring R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] {m n : ℕ} (le : m ≤ n) :
M ⧸ I ^ n • ⊤ →ₗ[R] M ⧸ I ^ m • ⊤

The linear map from M ⧸ I ^ m • ⊤ to M ⧸ I ^ n • ⊤ induced by the natural inclusion I ^ n • ⊤ → I ^ m • ⊤.

To future contributors: Before adding lemmas related to Submodule.factorPow, please check whether it can be generalized to Submodule.factor and whether the corresponding (more general) lemma for Submodule.factor already exists.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Submodule.factorPowSucc {R : Type u_1} [Ring R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (m : ℕ) :
    M ⧸ I ^ (m + 1) • ⊤ →ₗ[R] M ⧸ I ^ m • ⊤

    factorPow for n = m + 1

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Ideal.Quotient.factorPow {R : Type u_1} [Ring R] (I : Ideal R) [I.IsTwoSided] {m n : ℕ} (le : n ≤ m) :
      R ⧸ I ^ m →+* R ⧸ I ^ n

      The ring homomorphism from R ⧸ I ^ m to R ⧸ I ^ n induced by the natural inclusion I ^ n → I ^ m.

      To future contributors: Before adding lemmas related to Ideal.factorPow, please check whether it can be generalized to Ideal.factor and whether the corresponding (more general) lemma for Ideal.factor already exists.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Ideal.Quotient.factorPowSucc {R : Type u_1} [Ring R] (I : Ideal R) [I.IsTwoSided] (n : ℕ) :
        R ⧸ I ^ (n + 1) →+* R ⧸ I ^ n

        factorPow for m = n + 1

        Equations
        Instances For
          source
          theorem Ideal.map_mk_comap_factorPow {R : Type u_3} [CommRing R] (I : Ideal R) {a b : ℕ} (apos : 0 < a) (le : a ≤ b) :
          comap (Quotient.factorPow I le) (map (Quotient.mk (I ^ a)) I) = map (Quotient.mk (I ^ b)) I
          source
          theorem factorPowSucc.isUnit_of_isUnit_image {R : Type u_3} [CommRing R] {I : Ideal R} {n : ℕ} (npos : n > 0) {a : R ⧸ I ^ (n + 1)} (h : IsUnit ((Ideal.Quotient.factorPow I ⋯) a)) :
          IsUnit a