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

• DividedPowers.IsSubDPIdeal : 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.
• DividedPowers.SubDPIdeal : A bundled version of IsSubDPIdeal.
• DividedPowers.IsSubDPIdeal.dividedPowers: the divided power structure on a sub-dp-ideal.
• DividedPowers.IsSubDPIdeal.prod : if J is an A-ideal, then I ⬝ J is a sub-dp-ideal of I.
• DividedPowers.IsSubDPIdeal.span : the sub-dp-ideal of I generated by a set of elements of A.
• DividedPowers.subDPIdeal_inf_of_quot : if there is a dp-structure on I⬝(A/J) such that the quotient map is a dp-morphism, then J ⊓ I is a sub-dp-ideal of I.

Main results

• DividedPowers.isSubDPIdeal_inf_iff : the ideal J ⊓ I is a sub-dp-ideal of I if and only if (on I) the divided powers are compatible mod J.
• DividedPowers.span_isSubDPIdeal_iff : the span of a set S : Set A is a sub-dp-ideal of I if and only if for all n ∈ ℕ > 0 and all s ∈ S, hI.dpow n s ∈ span S.
• DividedPowers.isSubDPIdeal_ker : the kernel of a divided power morphism from I to J is a sub-dp-ideal of I.
• DividedPowers.isSubDPIdeal_map : the image of a divided power morphism from I to J is a sub-dp-ideal of J.

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.

TODO

• DividedPowers.SubDPIdeal.instCompleteLattice : sub-dp-ideals of I form a complete lattice under inclusion.
• DividedPowers.SubDPIdealspan_carrier_eq_dpow_span : 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.
• DividedPowers.Quotient.OfSurjective.dividedPowers: when f : A → B is a surjective map and 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.
• DividedPowers.Quotient.dividedPowers : 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.
• DividedPowers.Quotient.OfSurjective.dividedPowers_unique : the only divided power structure on I.map f such that the surjective map f : A → B is a divided power morphism is given by DividedPowers.Quotient.OfSurjective.dividedPowers.
• DividedPowers.Quotient.dividedPowers_unique : the only divided power structure on I(A⧸J) such that the quotient map A → A/J is a divided power morphism is given by DividedPowers.Quotient.dividedPowers.

References

• [P. Berthelot, Cohomologie cristalline des schémas de caractéristique $p$ > 0][Berthelot-1974]

• [P. Berthelot and A. Ogus, Notes on crystalline cohomology][BerthelotOgus-1978]

• [N. Roby, Lois polynomes et lois formelles en théorie des modules][Roby-1963]

• [N. Roby, Les algèbres à puissances dividées][Roby-1965]

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

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 ∈ J → hI.dpow n j ∈ J

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

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)] : DividedPowers J

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

Equations

• One or more equations did not get rendered due to their size.

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) : (dividedPowers hI hJ).IsDPMorphism hI (RingHom.id A)

theorem DividedPowers.isSubDPIdeal_inf_iff {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} : hI.IsSubDPIdeal (J ⊓ I) ↔ ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.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 compatiblity mod J. (The necessity was proved as a sanity check.)

theorem DividedPowers.span_isSubDPIdeal_iff {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {S : Set A} (hS : S ⊆ ↑I) : hI.IsSubDPIdeal (Ideal.span S) ↔ ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ Ideal.span S

[P. Berthelot and A. Ogus, Notes on crystalline cohomology (Lemma 3.6)][BerthelotOgus-1978]

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 (J ⊔ K)

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)) : hI.IsSubDPIdeal (iSup J)

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) : hJ.IsSubDPIdeal (Ideal.map f 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) : hJ.IsSubDPIdeal (Ideal.map f I)

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.

• carrier : Ideal A

  The underlying ideal.

• isSubideal : self.carrier ≤ I
• dpow_mem (n : ℕ) : n ≠ 0 → ∀ j ∈ self.carrier, hI.dpow n j ∈ self.carrier

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

theorem DividedPowers.SubDPIdeal.ext_iff {A : Type u_1} {inst✝ : CommSemiring A} {I : Ideal A} {hI : DividedPowers I} {x y : hI.SubDPIdeal} : x = y ↔ x.carrier = y.carrier

def DividedPowers.SubDPIdeal.mk' {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {J : Ideal A} (hJ : hI.IsSubDPIdeal J) : hI.SubDPIdeal

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

Equations

• DividedPowers.SubDPIdeal.mk' hJ = { carrier := J, isSubideal := ⋯, dpow_mem := ⋯ }

instance DividedPowers.SubDPIdeal.instSetLike {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} : SetLike hI.SubDPIdeal A

Equations

• DividedPowers.SubDPIdeal.instSetLike = { coe := fun (s : hI.SubDPIdeal) => ↑s.carrier, coe_injective' := ⋯ }

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

The coercion from SubDPIdeal to Ideal.

Equations

• ↑J = J.carrier

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

Equations

• DividedPowers.SubDPIdeal.instCoeOutIdeal = { coe := fun (J : hI.SubDPIdeal) => ↑J }

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

theorem DividedPowers.SubDPIdeal.toIsSubDPIdeal {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (J : hI.SubDPIdeal) : hI.IsSubDPIdeal J.carrier

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

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))][Berthelot-1974]

Equations

• DividedPowers.SubDPIdeal.prod J = { carrier := I • J, isSubideal := ⋯, dpow_mem := ⋯ }

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) : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)

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) : hI.SubDPIdeal

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

Equations

• DividedPowers.DPMorphism.ker hI hJ f = { carrier := RingHom.ker f.toRingHom ⊓ I, isSubideal := ⋯, dpow_mem := ⋯ }

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

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

Equations

• hI.dpEqualizer hI' = { carrier := {a : A | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

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.dpEqualizer_is_dp_ideal_left {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI hI' : DividedPowers I) : hI.IsSubDPIdeal (hI.dpEqualizer hI')

theorem DividedPowers.dpEqualizer_is_dp_ideal_right {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI hI' : DividedPowers I) : hI'.IsSubDPIdeal (hI.dpEqualizer hI')

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) : Ideal.map f I ≤ hK.dpEqualizer hK'

def DividedPowers.subDPIdeal_inf_of_quot {A : Type u_2} [CommRing A] {I : Ideal A} {hI : DividedPowers I} {J : Ideal A} {hJ : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)} {φ : hI.DPMorphism hJ} (hφ : φ.toRingHom = Ideal.Quotient.mk J) : hI.SubDPIdeal

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

• DividedPowers.subDPIdeal_inf_of_quot hφ = { carrier := J ⊓ I, isSubideal := ⋯, dpow_mem := ⋯ }