The square zero ideal of the trivial square-zero extension

• TrivSqZeroExt.kerIdeal: the ideal in the trivial square-zero extension

• TrivSqZeroExt.kerIdeal_sq : this ideal has square zero.

def TrivSqZeroExt.kerIdeal (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] : Ideal (TrivSqZeroExt R M)

The kernel of the AlgHom fstHom R R M

Equations

• TrivSqZeroExt.kerIdeal R M = RingHom.ker (TrivSqZeroExt.fstHom R R M)

theorem TrivSqZeroExt.mem_kerIdeal_iff_inr (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] (x : TrivSqZeroExt R M) : x ∈ kerIdeal R M ↔ x = inr x.snd

@[simp]

theorem TrivSqZeroExt.kerIdeal_sq (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] : kerIdeal R M ^ 2 = ⊥