Documentation

TauCeti.RingTheory.Ideal.Quotient.SquareZero

The p-th power map modulo a square-zero ideal #

Let B be a commutative ring in which a prime p is zero, and let I be an ideal of B with I ^ 2 = ⊥. Two lifts of an element of B ⧸ I differ by some i ∈ I, and i ^ p = 0, so their p-th powers agree. The p-th power map of B therefore factors through B ⧸ I as a ring homomorphism B ⧸ I →+* B.

Main definitions #

source
def Ideal.Quotient.powLift {B : Type u_1} [CommRing B] (p : ℕ) [hp : Fact (Nat.Prime p)] (hpB : ↑p = 0) {I : Ideal B} (hI : I ^ 2 = ⊥) :
B ⧸ I →+* B

Modulo a square-zero ideal of a ring in which p = 0, the p-th power of a lift does not depend on the lift: the p-th power map factors through B ⧸ I.

Instances For
    source
    @[simp]
    theorem Ideal.Quotient.powLift_mk {B : Type u_1} [CommRing B] (p : ℕ) [hp : Fact (Nat.Prime p)] (hpB : ↑p = 0) {I : Ideal B} (hI : I ^ 2 = ⊥) (b : B) :
    (powLift p hpB hI) ((mk I) b) = b ^ p

    powLift sends the class of b to b ^ p.

    source
    @[simp]
    theorem Ideal.Quotient.mk_powLift {B : Type u_1} [CommRing B] (p : ℕ) [hp : Fact (Nat.Prime p)] (hpB : ↑p = 0) {I : Ideal B} (hI : I ^ 2 = ⊥) (z : B ⧸ I) :
    (mk I) ((powLift p hpB hI) z) = z ^ p

    Reducing powLift p hpB hI z modulo I gives z ^ p.