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.
• 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.

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.
• DividedPowers.SubDPIdeal.instCompleteLattice : sub-dp-ideals of I form a complete lattice under inclusion.
• DividedPowers.SubDPIdeal.span_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_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.

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

• [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 compatibility 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_iff {A : Type u_1} {inst✝ : CommSemiring A} {I : Ideal A} {hI : DividedPowers I} {x y : hI.SubDPIdeal} : x = y ↔ x.carrier = y.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

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 := ⋯ }

instance DividedPowers.SubDPIdeal.instCoeOutElemIdealIic {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} : CoeOut hI.SubDPIdeal ↑(Set.Iic I)

Equations

• DividedPowers.SubDPIdeal.instCoeOutElemIdealIic = { coe := fun (J : hI.SubDPIdeal) => ⟨J.carrier, ⋯⟩ }

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

Equations

• DividedPowers.SubDPIdeal.instLE = { le := fun (J J' : hI.SubDPIdeal) => J.carrier ≤ J'.carrier }

theorem DividedPowers.SubDPIdeal.le_iff {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {J J' : hI.SubDPIdeal} : J ≤ J' ↔ J.carrier ≤ J'.carrier

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

Equations

• DividedPowers.SubDPIdeal.instLT = { lt := fun (J J' : hI.SubDPIdeal) => J.carrier < J'.carrier }

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

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

I is a sub-dp-ideal of itself.

Equations

• DividedPowers.SubDPIdeal.instTop = { top := { carrier := I, isSubideal := ⋯, dpow_mem := ⋯ } }

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

Equations

• DividedPowers.SubDPIdeal.inhabited = { default := ⊤ }

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

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

Equations

• DividedPowers.SubDPIdeal.instBot = { bot := { carrier := ⊥, isSubideal := ⋯, dpow_mem := ⋯ } }

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

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

Equations

• DividedPowers.SubDPIdeal.instMin = { min := fun (J J' : hI.SubDPIdeal) => { carrier := J.carrier ⊓ J'.carrier, isSubideal := ⋯, dpow_mem := ⋯ } }

theorem DividedPowers.SubDPIdeal.inf_carrier_def {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (J J' : hI.SubDPIdeal) : (J ⊓ J').carrier = J.carrier ⊓ J'.carrier

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

Equations

• DividedPowers.SubDPIdeal.instInfSet = { sInf := fun (S : Set hI.SubDPIdeal) => { carrier := ⨅ s ∈ insert ⊤ S, s.carrier, isSubideal := ⋯, dpow_mem := ⋯ } }

theorem DividedPowers.SubDPIdeal.sInf_carrier_def {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (S : Set hI.SubDPIdeal) : (sInf S).carrier = ⨅ s ∈ insert ⊤ S, s.carrier

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

Equations

• DividedPowers.SubDPIdeal.instMax = { max := fun (J J' : hI.SubDPIdeal) => DividedPowers.SubDPIdeal.mk' ⋯ }

theorem DividedPowers.SubDPIdeal.sup_carrier_def {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (J J' : hI.SubDPIdeal) : (J ⊔ J').carrier = ↑⟨(J ⊔ J').carrier, ⋯⟩

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

Equations

• DividedPowers.SubDPIdeal.instSupSet = { sSup := fun (S : Set hI.SubDPIdeal) => DividedPowers.SubDPIdeal.mk' ⋯ }

theorem DividedPowers.SubDPIdeal.sSup_carrier_def {A : Type u_1} [CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (S : Set hI.SubDPIdeal) : (sSup S).carrier = sSup (toIdeal '' S)

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

Equations

• DividedPowers.SubDPIdeal.instCompleteLattice = Function.Injective.completeLattice (fun (J : hI.SubDPIdeal) => ⟨J.carrier, ⋯⟩) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def DividedPowers.SubDPIdeal.span {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) (S : Set A) : hI.SubDPIdeal

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

Equations

• DividedPowers.SubDPIdeal.span hI S = sInf {J : hI.SubDPIdeal | S ⊆ ↑J.carrier}

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) : 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 := ⋯ }

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) : ℕ → B → B

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

• DividedPowers.Quotient.OfSurjective.dpow hI f n = Function.extend (fun (a : ↥I) => f ↑a) (fun (a : ↥I) => f (hI.dpow n ↑a)) 0

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 f ⊓ I)) {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 f ⊓ I)) : DividedPowers J

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.

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 f ⊓ I)) {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 f ⊓ I)) {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 f ⊓ I)) : 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 f ⊓ I)) (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 ⧸ J → A ⧸ 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

• DividedPowers.Quotient.dpow hI J = DividedPowers.Quotient.OfSurjective.dpow hI (Ideal.Quotient.mk J)

noncomputable def DividedPowers.Quotient.dividedPowers {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} (hIJ : hI.IsSubDPIdeal (J ⊓ I)) : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)

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

• DividedPowers.Quotient.dividedPowers hI hIJ = DividedPowers.Quotient.OfSurjective.dividedPowers hI ⋯ ⋯ ⋯

theorem DividedPowers.Quotient.dpow_apply {A : Type u_1} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} (hIJ : hI.IsSubDPIdeal (J ⊓ I)) {n : ℕ} {a : A} (ha : a ∈ I) : (dividedPowers hI hIJ).dpow n ((Ideal.Quotient.mk J) a) = (Ideal.Quotient.mk J) (hI.dpow n a)

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 (J ⊓ I)) : hI.IsDPMorphism (dividedPowers hI hIJ) (Ideal.Quotient.mk J)

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