Divided power morphisms

Let A and B be commutative (semi)rings, let I be an ideal of A and let J be an ideal of B. Given divided power structures on I and J, a ring morphism A →+* B is a divided power morphism if it is compatible with these divided power structures.

Main definitions

• DividedPowers.IsDPMorphism : given divided power structures on the A-ideal I and the B-ideal J, a ring morphism A →+* B is a divided power morphism if it is compatible with these divided power structures.
• DividedPowers.DPMorphism : a bundled version of IsDPMorphism.
• DividedPowers.ideal_from_ringHom : given a ring homomorphism A →+* B and ideals I ⊆ A and J ⊆ B such that I.map f ≤ J, this is the A-ideal on which f (hI.dpow n x) = hJ.dpow n (f x).
• DividedPowers.DPMorphism.fromGens : the DPMorphism induced by a ring morphism, given that divided powers are compatible on a generating set.

Main results

• DividedPowers.dpow_eq_from_gens : if two divided power structures on an ideal I agree on a generating set, then they are equal.

Implementation remarks

We provided both a bundled and an unbundled definition of divided power morphisms. For developing the basic theory, the unbundled version IsDPMorphism is more convenient. However, we anticipate that the bundled version DPMorphism will be better for the development of crystalline cohomology.

References

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

• P. Berthelot and A. Ogus, Notes on crystalline cohomology

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

• N. Roby, Les algèbres à puissances dividées

structure DividedPowers.IsDPMorphism {A : Type u_1} {B : Type u_2} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} (hI : DividedPowers I) (hJ : DividedPowers J) (f : A →+* B) : Prop

Given divided power structures on the A-ideal I and the B-ideal J, a ring morphism A → B is a divided power morphism if it is compatible with these divided power structures.

• ideal_comp : Ideal.map f I ≤ J
• dpow_comp {n : ℕ} (a : A) : a ∈ I → hJ.dpow n (f a) = f (hI.dpow n a)

theorem DividedPowers.isDPMorphism_def {A : Type u_1} {B : Type u_2} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} (hI : DividedPowers I) (hJ : DividedPowers J) (f : A →+* B) : hI.IsDPMorphism hJ f ↔ Ideal.map f I ≤ J ∧ ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)

theorem DividedPowers.isDPMorphism_iff {A : Type u_1} {B : Type u_2} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} (hI : DividedPowers I) (hJ : DividedPowers J) (f : A →+* B) : hI.IsDPMorphism hJ f ↔ Ideal.map f I ≤ J ∧ ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)

theorem DividedPowers.IsDPMorphism.map_dpow {A : Type u_1} {B : Type u_2} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} {hI : DividedPowers I} {hJ : DividedPowers J} {f : A →+* B} (hf : hI.IsDPMorphism hJ f) {n : ℕ} {a : A} (ha : a ∈ I) : f (hI.dpow n a) = hJ.dpow n (f a)

theorem DividedPowers.IsDPMorphism.comp {A : Type u_1} {B : Type u_2} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} {hI : DividedPowers I} {hJ : DividedPowers J} {C : Type u_3} [CommSemiring C] {K : Ideal C} (hK : DividedPowers K) {f : A →+* B} {g : B →+* C} (hg : hJ.IsDPMorphism hK g) (hf : hI.IsDPMorphism hJ f) : hI.IsDPMorphism hK (g.comp f)

structure DividedPowers.DPMorphism {A : Type u_3} {B : Type u_4} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} (hI : DividedPowers I) (hJ : DividedPowers J) extends A →+* B : Type (max u_3 u_4)

A bundled divided power morphism between rings endowed with divided power structures.

• toFun : A → B
• map_one' : (↑↑self.toRingHom).toFun 1 = 1
• map_mul' (x y : A) : (↑↑self.toRingHom).toFun (x * y) = (↑↑self.toRingHom).toFun x * (↑↑self.toRingHom).toFun y
• map_zero' : (↑↑self.toRingHom).toFun 0 = 0
• map_add' (x y : A) : (↑↑self.toRingHom).toFun (x + y) = (↑↑self.toRingHom).toFun x + (↑↑self.toRingHom).toFun y
• ideal_comp : Ideal.map self.toRingHom I ≤ J
• dpow_comp {n : ℕ} (a : A) : a ∈ I → hJ.dpow n (self.toRingHom a) = self.toRingHom (hI.dpow n a)

theorem DividedPowers.DPMorphism.ext {A : Type u_3} {B : Type u_4} {inst✝ : CommSemiring A} {inst✝¹ : CommSemiring B} {I : Ideal A} {J : Ideal B} {hI : DividedPowers I} {hJ : DividedPowers J} {x y : hI.DPMorphism hJ} (toFun : (↑↑x.toRingHom).toFun = (↑↑y.toRingHom).toFun) : x = y

instance DividedPowers.DPMorphism.instFunLike {A : Type u_3} {B : Type u_4} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} (hI : DividedPowers I) (hJ : DividedPowers J) : FunLike (hI.DPMorphism hJ) A B

Equations

• DividedPowers.DPMorphism.instFunLike hI hJ = { coe := fun (h : hI.DPMorphism hJ) => ⇑h.toRingHom, coe_injective' := ⋯ }

instance DividedPowers.DPMorphism.coe_ringHom {A : Type u_3} {B : Type u_4} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} (hI : DividedPowers I) (hJ : DividedPowers J) : CoeOut (hI.DPMorphism hJ) (A →+* B)

Equations

• DividedPowers.DPMorphism.coe_ringHom hI hJ = { coe := DividedPowers.DPMorphism.toRingHom }

@[simp]

theorem DividedPowers.DPMorphism.coe_toRingHom {A : Type u_3} {B : Type u_4} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} (hI : DividedPowers I) (hJ : DividedPowers J) {f : hI.DPMorphism hJ} : ⇑f.toRingHom = ⇑f

@[simp]

theorem DividedPowers.DPMorphism.toRingHom_apply {A : Type u_3} {B : Type u_4} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} (hI : DividedPowers I) (hJ : DividedPowers J) {f : hI.DPMorphism hJ} {a : A} : f.toRingHom a = f a

theorem DividedPowers.DPMorphism.isDPMorphism {A : Type u_3} {B : Type u_4} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} {hI : DividedPowers I} {hJ : DividedPowers J} (f : hI.DPMorphism hJ) : hI.IsDPMorphism hJ f.toRingHom

def DividedPowers.DPMorphism.mk' {A : Type u_3} {B : Type u_4} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} {hI : DividedPowers I} {hJ : DividedPowers J} {f : A →+* B} (hf : hI.IsDPMorphism hJ f) : hI.DPMorphism hJ

A constructor for DPMorphism from a ring homomorphism f : A →+* B satisfying IsDPMorphism hI hJ f.

Equations

• DividedPowers.DPMorphism.mk' hf = { toRingHom := f, ideal_comp := ⋯, dpow_comp := ⋯ }

def DividedPowers.ideal_from_ringHom {A : Type u_3} {B : Type u_4} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} (hI : DividedPowers I) (hJ : DividedPowers J) {f : A →+* B} (hf : Ideal.map f I ≤ J) : Ideal A

Given a ring homomorphism A → B and ideals I ⊆ A and J ⊆ B such that I.map f ≤ J, this is the A-ideal on which f (hI.dpow n x) = hJ.dpow n (f x). See N. Roby, Les algèbres à puissances dividées (Proposition 2).

Equations

• hI.ideal_from_ringHom hJ hf = { carrier := {x : A | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def DividedPowers.DPMorphism.fromGens {A : Type u_3} {B : Type u_4} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} (hI : DividedPowers I) (hJ : DividedPowers J) {f : A →+* B} {S : Set A} (hS : I = Ideal.span S) (hf : Ideal.map f I ≤ J) (h : ∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)) : hI.DPMorphism hJ

The DPMorphism induced by a ring morphism, given that divided powers are compatible on a generating set. See N. Roby, Les algèbres à puissances dividées (Proposition 3).

Equations

• DividedPowers.DPMorphism.fromGens hI hJ hS hf h = { toRingHom := f, ideal_comp := hf, dpow_comp := ⋯ }

def DividedPowers.DPMorphism.id {A : Type u_3} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) : hI.DPMorphism hI

The identity map as a DPMorphism.

Equations

• DividedPowers.DPMorphism.id hI = { toRingHom := RingHom.id A, ideal_comp := ⋯, dpow_comp := ⋯ }

instance DividedPowers.DPMorphism.instInhabited {A : Type u_3} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) : Inhabited (hI.DPMorphism hI)

Equations

• DividedPowers.DPMorphism.instInhabited hI = { default := DividedPowers.DPMorphism.id hI }

theorem DividedPowers.DPMorphism.fromGens_coe {A : Type u_3} {B : Type u_4} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} (hI : DividedPowers I) (hJ : DividedPowers J) {f : A →+* B} {S : Set A} (hS : I = Ideal.span S) (hf : Ideal.map f I ≤ J) (h : ∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)) : (fromGens hI hJ hS hf ⋯).toRingHom = f

theorem DividedPowers.IsDPMorphism.on_span {A : Type u_3} {B : Type u_4} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} (hI : DividedPowers I) (hJ : DividedPowers J) {f : A →+* B} {S : Set A} (hS : I = Ideal.span S) (hS' : ∀ s ∈ S, f s ∈ J) (hdp : ∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)) : hI.IsDPMorphism hJ f

theorem DividedPowers.IsDPMorphism.of_comp {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring A] [CommSemiring B] [CommSemiring C] {I : Ideal A} {J : Ideal B} {K : Ideal C} (hI : DividedPowers I) (hJ : DividedPowers J) (hK : DividedPowers K) (f : A →+* B) (g : B →+* C) (heq : J = Ideal.map f I) (hf : hI.IsDPMorphism hJ f) (hh : hI.IsDPMorphism hK (g.comp f)) : hJ.IsDPMorphism hK g

def DividedPowers.DPMorphism.comp {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring A] [CommSemiring B] [CommSemiring C] {I : Ideal A} {J : Ideal B} {K : Ideal C} {hI : DividedPowers I} {hJ : DividedPowers J} {hK : DividedPowers K} (g : hJ.DPMorphism hK) (f : hI.DPMorphism hJ) : hI.DPMorphism hK

The composition of two divided power morphisms as a DPMorphism.

Equations

• g.comp f = DividedPowers.DPMorphism.mk' ⋯

@[simp]

theorem DividedPowers.DPMorphism.comp_toRingHom {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring A] [CommSemiring B] [CommSemiring C] {I : Ideal A} {J : Ideal B} {K : Ideal C} {hI : DividedPowers I} {hJ : DividedPowers J} {hK : DividedPowers K} (g : hJ.DPMorphism hK) (f : hI.DPMorphism hJ) : (g.comp f).toRingHom = g.comp f.toRingHom

theorem DividedPowers.dpow_comp_from_gens {A : Type u_3} {B : Type u_4} [CommSemiring A] [CommSemiring B] {I : Ideal A} {J : Ideal B} (hI : DividedPowers I) (hJ : DividedPowers J) {f : A →+* B} {S : Set A} (hS : I = Ideal.span S) (hS' : ∀ s ∈ S, f s ∈ J) (hdp : ∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)) {n : ℕ} (a : A) : a ∈ I → hJ.dpow n (f a) = f (hI.dpow n a)

theorem DividedPowers.dpow_eq_from_gens {A : Type u_3} [CommSemiring A] {I : Ideal A} (hI hI' : DividedPowers I) {S : Set A} (hS : I = Ideal.span S) (hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a) : hI' = hI

If two divided power structures on the ideal I agree on a generating set, then they are equal. See N. Roby, Les algèbres à puissances dividées (Corollary to Proposition 3).