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-idealJ
of a divided power ideal(I, hI)
is a sub-dp-ideal if for alln > 0
and allx ∈ J
,hI.dpow n j ∈ J
.DividedPowers.SubDPIdeal
: A bundled version ofIsSubDPIdeal
.DividedPowers.IsSubDPIdeal.dividedPowers
: the divided power structure on a sub-dp-ideal.DividedPowers.IsSubDPIdeal.prod
: ifJ
is anA
-ideal, thenI ⬝ J
is a sub-dp-ideal ofI
.DividedPowers.IsSubDPIdeal.span
: the sub-dp-ideal ofI
generated by a set of elements ofA
.DividedPowers.subDPIdeal_inf_of_quot
: if there is a dp-structure onI⬝(A/J)
such that the quotient map is a dp-morphism, thenJ ⊓ I
is a sub-dp-ideal ofI
.DividedPowers.Quotient.OfSurjective.dividedPowers
: whenf : A → B
is a surjective map andf.ker ⊓ I
is a sub-dp-ideal ofI
, this is the induced divided power structure on the idealI.map f
of the target.DividedPowers.Quotient.dividedPowers
: whenI ⊓ J
is a sub-dp-ideal ofI
, this is the divided power structure on the idealI(A⧸J)
of the quotient.
Main results #
DividedPowers.isSubDPIdeal_inf_iff
: the idealJ ⊓ I
is a sub-dp-ideal ofI
if and only if (onI
) the divided powers are compatible modJ
.DividedPowers.span_isSubDPIdeal_iff
: the span of a setS : Set A
is a sub-dp-ideal ofI
if and only if for alln ∈ ℕ > 0
and alls ∈ S
, hI.dpow n s ∈ span S.DividedPowers.isSubDPIdeal_ker
: the kernel of a divided power morphism fromI
toJ
is a sub-dp-ideal ofI
.DividedPowers.isSubDPIdeal_map
: the image of a divided power morphism fromI
toJ
is a sub-dp-ideal ofJ
.DividedPowers.SubDPIdeal.instCompleteLattice
: sub-dp-ideals ofI
form a complete lattice under inclusion.DividedPowers.SubDPIdealspan_carrier_eq_dpow_span
: the underlying ideal ofSubDPIdeal.span hI S
is generated by the elements of the formhI.dpow n x
withn > 0
andx ∈ S
.DividedPowers.Quotient.OfSurjective.dividedPowers_unique
: the only divided power structure onI.map f
such that the surjective mapf : A → B
is a divided power morphism is given byDividedPowers.Quotient.OfSurjective.dividedPowers
.DividedPowers.Quotient.dividedPowers_unique
: the only divided power structure onI(A⧸J)
such that the quotient mapA → A/J
is a divided power morphism is given byDividedPowers.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 #
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
.
Instances For
The divided power structure on a sub-dp-ideal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.)
P. Berthelot and A. Ogus, Notes on crystalline cohomology (Lemma 3.6)
The image of a divided power morphism from I
to J
is a sub-dp-ideal of J
.
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.
Instances For
Constructs a SubPDIdeal
given an ideal J
satisfying hI.IsSubDPIdeal J
.
Equations
- DividedPowers.SubDPIdeal.mk' hJ = { carrier := J, isSubideal := ⋯, dpow_mem := ⋯ }
Instances For
Equations
- DividedPowers.SubDPIdeal.instSetLike = { coe := fun (s : hI.SubDPIdeal) => ↑s.carrier, coe_injective' := ⋯ }
The coercion from SubDPIdeal
to Ideal
.
Instances For
Equations
- DividedPowers.SubDPIdeal.instCoeOutIdeal = { coe := fun (J : hI.SubDPIdeal) => ↑J }
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
- DividedPowers.SubDPIdeal.prod J = { carrier := I • J, isSubideal := ⋯, dpow_mem := ⋯ }
Instances For
Equations
- DividedPowers.SubDPIdeal.instCoeOutElemIdealIic = { coe := fun (J : hI.SubDPIdeal) => ⟨J.carrier, ⋯⟩ }
Equations
- DividedPowers.SubDPIdeal.instLE = { le := fun (J J' : hI.SubDPIdeal) => J.carrier ≤ J'.carrier }
Equations
- DividedPowers.SubDPIdeal.instLT = { lt := fun (J J' : hI.SubDPIdeal) => J.carrier < J'.carrier }
I is a sub-dp-ideal ot itself.
Equations
- DividedPowers.SubDPIdeal.inhabited = { default := ⊤ }
(0)
is a sub-dp-ideal ot the dp-ideal I
.
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 := ⋯ } }
Equations
- DividedPowers.SubDPIdeal.instMax = { max := fun (J J' : hI.SubDPIdeal) => DividedPowers.SubDPIdeal.mk' ⋯ }
Equations
- DividedPowers.SubDPIdeal.instSupSet = { sSup := fun (S : Set hI.SubDPIdeal) => DividedPowers.SubDPIdeal.mk' ⋯ }
Equations
- DividedPowers.SubDPIdeal.instCompleteLattice = Function.Injective.completeLattice (fun (J : hI.SubDPIdeal) => ⟨J.carrier, ⋯⟩) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
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}
Instances For
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
.
The kernel of a divided power morphism from I
to J
is a sub-dp-ideal of I
.
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 := ⋯ }
Instances For
The ideal of A
in which the two divided power structures hI
and hI'
coincide.
Equations
Instances For
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 := ⋯ }
Instances For
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
Instances For
Divided powers on the the codomain B
of a surjective ring homomorphism f
are compatible
with f
.
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
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
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
Divided powers on the quotient are compatible with quotient map