Documentation

Mathlib.RingTheory.DividedPowers.SubDPIdeal

Sub-divided power-ideals #

Let A be a commutative (semi)ring and let I be an ideal of A with a divided power structure hI. A subideal J of I is a sub-dp-ideal of (I, hI) if, for all n ∈ ℕ > 0 and all x ∈ J, hI.dpow n x ∈ J.

Main definitions #

Main results #

Implementation remarks #

We provide both a bundled and an unbundled definition of sub-dp-ideals. The unbundled version is often more convenient when a larger proof requires to show that a certain ideal is a sub-dp-ideal. On the other hand, a bundled version is required to prove that sub-dp-ideals form a complete lattice.

References #

structure DividedPowers.IsSubDPIdeal {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) (J : Ideal A) :

A sub-ideal J of a divided power ideal (I, hI) is a sub-dp-ideal if for all n > 0 and all x ∈ J, hI.dpow n j ∈ J.

  • isSubideal : J I
  • dpow_mem (n : ) : n 0∀ {j : A}, j JhI.dpow n j J
Instances For
    def DividedPowers.IsSubDPIdeal.dividedPowers {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} (hJ : hI.IsSubDPIdeal J) [(x : A) → Decidable (x J)] :

    The divided power structure on a sub-dp-ideal.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem DividedPowers.IsSubDPIdeal.dpow_eq {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} (hJ : hI.IsSubDPIdeal J) [(x : A) → Decidable (x J)] (n : ) (a : A) :
      (dividedPowers hI hJ).dpow n a = if a J then hI.dpow n a else 0
      theorem DividedPowers.IsSubDPIdeal.dpow_eq_of_mem {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} (hJ : hI.IsSubDPIdeal J) [(x : A) → Decidable (x J)] {n : } {a : A} (ha : a J) :
      (dividedPowers hI hJ).dpow n a = hI.dpow n a
      theorem DividedPowers.IsSubDPIdeal.isDPMorphism {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} [(x : A) → Decidable (x J)] (hJ : hI.IsSubDPIdeal J) :
      theorem DividedPowers.isSubDPIdeal_inf_iff {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} :
      hI.IsSubDPIdeal (JI) ∀ {n : } {a b : A}, a Ib Ia - b JhI.dpow n a - hI.dpow n b J

      The ideal J ⊓ I is a sub-dp-ideal of I if and only if the divided powers have some compatibility mod J. (The necessity was proved as a sanity check.)

      theorem DividedPowers.isSubDPIdeal_sup {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {J K : Ideal A} (hJ : hI.IsSubDPIdeal J) (hK : hI.IsSubDPIdeal K) :
      hI.IsSubDPIdeal (JK)
      theorem DividedPowers.isSubDPIdeal_iSup {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {ι : Type u_3} {J : ιIdeal A} (hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)) :
      theorem DividedPowers.isSubDPIdeal_iInf {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {ι : Type u_3} {J : ιIdeal A} (hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)) :
      hI.IsSubDPIdeal (I⨅ (i : ι), J i)
      theorem DividedPowers.isSubDPIdeal_map_of_isSubDPIdeal {A : Type u_1} {B : Type u_2} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} [CommSemiring B] {J : Ideal B} {hJ : DividedPowers J} {f : A →+* B} (hf : hI.IsDPMorphism hJ f) {K : Ideal A} (hK : hI.IsSubDPIdeal K) :
      theorem DividedPowers.isSubDPIdeal_map {A : Type u_1} {B : Type u_2} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} [CommSemiring B] {J : Ideal B} {hJ : DividedPowers J} {f : A →+* B} (hf : hI.IsDPMorphism hJ f) :

      The image of a divided power morphism from I to J is a sub-dp-ideal of J.

      structure DividedPowers.SubDPIdeal {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) :
      Type u_1

      A SubDPIdeal of I is a sub-ideal J of I such that for all n > 0 x ∈ J, hI.dpow n j ∈ J. The unbundled version of this definition is called IsSubDPIdeal.

      Instances For
        theorem DividedPowers.SubDPIdeal.ext_iff {A : Type u_1} {inst✝ : CommSemiring A} {I : Ideal A} {hI : DividedPowers I} {x y : hI.SubDPIdeal} :
        theorem DividedPowers.SubDPIdeal.ext {A : Type u_1} {inst✝ : CommSemiring A} {I : Ideal A} {hI : DividedPowers I} {x y : hI.SubDPIdeal} (carrier : x.carrier = y.carrier) :
        x = y
        def DividedPowers.SubDPIdeal.mk' {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {J : Ideal A} (hJ : hI.IsSubDPIdeal J) :

        Constructs a SubPDIdeal given an ideal J satisfying hI.IsSubDPIdeal J.

        Equations
        Instances For
          Equations

          The coercion from SubDPIdeal to Ideal.

          Equations
          Instances For
            theorem DividedPowers.SubDPIdeal.coe_def {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (J : hI.SubDPIdeal) :
            J = J.carrier
            @[simp]
            theorem DividedPowers.SubDPIdeal.memCarrier {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {s : hI.SubDPIdeal} {x : A} :
            x s.carrier x s
            def DividedPowers.SubDPIdeal.prod {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (J : Ideal A) :

            If J is an ideal of A, then I⬝J is a sub-dp-ideal of I. See P. Berthelot, Cohomologie cristalline des schémas de caractéristique $p$ > 0, (Proposition 1.6.1 (i))

            Equations
            Instances For
              Equations
              theorem DividedPowers.SubDPIdeal.le_iff {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {J J' : hI.SubDPIdeal} :
              Equations
              theorem DividedPowers.SubDPIdeal.lt_iff {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {J J' : hI.SubDPIdeal} :
              J < J' J.carrier < J'.carrier

              I is a sub-dp-ideal ot itself.

              Equations

              (0) is a sub-dp-ideal ot the dp-ideal I.

              Equations

              The intersection of two sub-dp-ideals is a sub-dp-ideal.

              Equations
              theorem DividedPowers.SubDPIdeal.inf_carrier_def {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (J J' : hI.SubDPIdeal) :
              (JJ').carrier = J.carrierJ'.carrier
              Equations
              theorem DividedPowers.SubDPIdeal.sup_carrier_def {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (J J' : hI.SubDPIdeal) :
              (JJ').carrier = (JJ').carrier,
              def DividedPowers.SubDPIdeal.span {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) (S : Set A) :

              The sub-dp-ideal of I generated by a family of elements of A.

              Equations
              Instances For
                theorem DividedPowers.dpow_span_isSubideal {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {S : Set A} (hS : S I) :
                Ideal.span {y : A | ∃ (n : ) (_ : n 0) (x : A) (_ : x S), y = hI.dpow n x} I
                theorem DividedPowers.SubDPIdeal.dpow_mem_span_of_mem_span {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {S : Set A} (hS : S I) {k : } (hk : k 0) {z : A} (hz : z Ideal.span {y : A | ∃ (n : ) (_ : n 0) (x : A) (_ : x S), y = hI.dpow n x}) :
                hI.dpow k z Ideal.span {y : A | ∃ (n : ) (_ : n 0) (x : A) (_ : x S), y = hI.dpow n x}
                theorem DividedPowers.SubDPIdeal.span_carrier_eq_dpow_span {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {S : Set A} (hS : S I) :
                (SubDPIdeal.span hI S).carrier = Ideal.span {y : A | ∃ (n : ) (_ : n 0) (x : A) (_ : x S), y = hI.dpow n x}

                The underlying ideal of SubDPIdeal.span hI S is generated by the elements of the form hI.dpow n x with n > 0 and x ∈ S.

                theorem DividedPowers.isSubDPIdeal_ker {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [CommRing B] {J : Ideal B} (hJ : DividedPowers J) {f : A →+* B} (hf : hI.IsDPMorphism hJ f) :

                The kernel of a divided power morphism from I to J is a sub-dp-ideal of I.

                def DividedPowers.DPMorphism.ker {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [CommRing B] {J : Ideal B} (hJ : DividedPowers J) (f : hI.DPMorphism hJ) :

                The kernel of a divided power morphism, as a SubDPIdeal.

                Equations
                Instances For
                  def DividedPowers.dpEqualizer {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI hI' : DividedPowers I) :

                  The ideal of A in which the two divided power structures hI and hI' coincide.

                  Equations
                  Instances For
                    theorem DividedPowers.mem_dpEqualizer_iff {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI hI' : DividedPowers I) {x : A} :
                    x hI.dpEqualizer hI' x I ∀ (n : ), hI.dpow n x = hI'.dpow n x
                    theorem DividedPowers.le_equalizer_of_isDPMorphism {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [CommSemiring B] (f : A →+* B) {K : Ideal B} (hI_le_K : Ideal.map f I K) (hK hK' : DividedPowers K) (hIK : hI.IsDPMorphism hK f) (hIK' : hI.IsDPMorphism hK' f) :

                    If there is a divided power structure on I⬝(A/J) such that the quotient map is a dp-morphism, then J ⊓ I is a sub-dp-ideal of I.

                    Equations
                    Instances For
                      noncomputable def DividedPowers.Quotient.OfSurjective.dpow {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [CommRing B] (f : A →+* B) :
                      BB

                      The definition of divided powers on the codomain B of a surjective ring homomorphism from a ring A with divided powers hI. This definition is tagged as noncomputable because it makes use of Function.extend, but under the hypothesis IsSubDPIdeal hI (RingHom.ker f ⊓ I), dividedPowers_unique proves that no choices are involved.

                      Equations
                      Instances For
                        theorem DividedPowers.Quotient.OfSurjective.dpow_apply' {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [CommRing B] {f : A →+* B} (hIf : hI.IsSubDPIdeal (RingHom.ker fI)) {n : } {a : A} (ha : a I) :
                        dpow hI f n (f a) = f (hI.dpow n a)

                        Divided powers on the the codomain B of a surjective ring homomorphism f are compatible with f.

                        noncomputable def DividedPowers.Quotient.OfSurjective.dividedPowers {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [CommRing B] {f : A →+* B} {J : Ideal B} (hf : Function.Surjective f) (hIJ : J = Ideal.map f I) (hIf : hI.IsSubDPIdeal (RingHom.ker fI)) :

                        When f.ker ⊓ I is a sub-dp-ideal of I, this is the induced divided power structure on the ideal I.map f of the target.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem DividedPowers.Quotient.OfSurjective.dpow_def {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [CommRing B] {f : A →+* B} {J : Ideal B} (hf : Function.Surjective f) (hIJ : J = Ideal.map f I) (hIf : hI.IsSubDPIdeal (RingHom.ker fI)) {n : } {x : B} :
                          (dividedPowers hI hf hIJ hIf).dpow n x = dpow hI f n x
                          theorem DividedPowers.Quotient.OfSurjective.dpow_apply {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [CommRing B] {f : A →+* B} {J : Ideal B} (hf : Function.Surjective f) (hIJ : J = Ideal.map f I) (hIf : hI.IsSubDPIdeal (RingHom.ker fI)) {n : } {a : A} (ha : a I) :
                          (dividedPowers hI hf hIJ hIf).dpow n (f a) = f (hI.dpow n a)
                          theorem DividedPowers.Quotient.OfSurjective.isDPMorphism {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [CommRing B] {f : A →+* B} {J : Ideal B} (hf : Function.Surjective f) (hIJ : J = Ideal.map f I) (hIf : hI.IsSubDPIdeal (RingHom.ker fI)) :
                          hI.IsDPMorphism (dividedPowers hI hf hIJ hIf) f
                          theorem DividedPowers.Quotient.OfSurjective.dividedPowers_unique {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [CommRing B] {f : A →+* B} {J : Ideal B} (hf : Function.Surjective f) (hIJ : J = Ideal.map f I) (hIf : hI.IsSubDPIdeal (RingHom.ker fI)) (hquot : DividedPowers J) (hm : hI.IsDPMorphism hquot f) :
                          hquot = dividedPowers hI hf hIJ hIf
                          noncomputable def DividedPowers.Quotient.dpow {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) (J : Ideal A) :
                          A JA J

                          The definition of divided powers on A ⧸ J. Tagged as noncomputable because it makes use of Function.extend, but under IsSubDPIdeal hI (J ⊓ I), dividedPowers_unique proves that no choices are involved.

                          Equations
                          Instances For
                            noncomputable def DividedPowers.Quotient.dividedPowers {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} (hIJ : hI.IsSubDPIdeal (JI)) :

                            When I ⊓ J is a sub-dp-ideal of I, this is the divided power structure on the ideal I(A⧸J) of the quotient.

                            Equations
                            Instances For
                              theorem DividedPowers.Quotient.dpow_apply {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} (hIJ : hI.IsSubDPIdeal (JI)) {n : } {a : A} (ha : a I) :

                              Divided powers on the quotient are compatible with quotient map

                              theorem DividedPowers.Quotient.isDPMorphism {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} (hIJ : hI.IsSubDPIdeal (JI)) :
                              theorem DividedPowers.Quotient.dividedPowers_unique {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} (hIJ : hI.IsSubDPIdeal (JI)) (hquot : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)) (hm : hI.IsDPMorphism hquot (Ideal.Quotient.mk J)) :
                              hquot = dividedPowers hI hIJ