PDSquareZeroResidue.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.PDSquareZero.residueQuotientEquiv line 12

Source documentation

The radical quotient is unchanged by a square-zero kernel.

def residueQuotientEquiv (f : A →+* D) (hf : Function.Surjective f)
    (hsq : ∀ a ∈ RingHom.ker f, ∀ b ∈ RingHom.ker f, a*b=0) :
    A ⧸ Ring.jacobson A ≃+* D ⧸ Ring.jacobson D := by
…

theorem OAI.LittleFinitistic.PDSquareZero.residueQuotientEquiv_mk line 25

theorem OAI.LittleFinitistic.PDSquareZero.kernel_annihilates_simple line 32

Source documentation

The nilpotent ideal annihilates every actual simple left A-module.

theorem kernel_annihilates_simple (f : A →+* D)
    (hsq : ∀ a ∈ RingHom.ker f, ∀ b ∈ RingHom.ker f, a*b=0)
    (S : Type u) [AddCommGroup S] [Module A S] [IsSimpleModule A S]
    (a : A) (ha : a ∈ RingHom.ker f) (s : S) : a • s=0 :=
…

def OAI.LittleFinitistic.PDSquareZero.squareZeroResidueEquiv line 46
Source documentation
The exact quotient-ring isomorphism S in Section 6.
```
def squareZeroResidueEquiv :
    TrivSqZeroExt D X ⧸ Ring.jacobson (TrivSqZeroExt D X) ≃+* D ⧸ Ring.jacobson D :=
…
```
theorem OAI.LittleFinitistic.PDSquareZero.squareZeroResidueEquiv_mk line 52