Augmentation ideals

• Ideal.IsAugmentation : An ideal I of an A-algebra S is an augmentation ideal if its underlying submodule is a complement of 1 : Submodule A S.

• Ideal.isAugmentation_subalgebra_iff : If S is a subalgebra of an R-algebra A, then an ideal Iof A is an augmentation ideal for the R-algebra structure if and only if it is an augmentation ideal for the S-algebra structure.

def Ideal.IsAugmentation (R : Type u_1) [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (I : Ideal A) : Prop

An ideal I of an R-algebra A is an augmentation ideal if its underlying module is a complement to 1 : Submodule R A.

Equations

• Ideal.IsAugmentation R I = IsCompl 1 (Submodule.restrictScalars R I)

theorem Ideal.isAugmentation_iff (R : Type u_1) [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (I : Ideal A) : IsAugmentation R I ↔ IsCompl 1 (Submodule.restrictScalars R I)

theorem Ideal.isAugmentation_subalgebra_iff (R : Type u_1) [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {S : Subalgebra R A} {I : Ideal A} : IsAugmentation (↥S) I ↔ IsCompl (Subalgebra.toSubmodule S) (Submodule.restrictScalars R I)

If S is a subalgebra of an R-algebra A, then an ideal Iof A is an augmentation ideal for the R-algebra structure if and only if it is an augmentation ideal for the S-algebra structure.