PDSquareZero.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.PDSquareZero.squareZero_le_jacobson line 12
Source documentation
A square-zero ideal lies in the actual noncommutative Jacobson radical.
```
theorem squareZero_le_jacobson (I : Ideal A)
    (hI : ∀ a ∈ I, ∀ b ∈ I, a*b=0) : I ≤ Ring.jacobson A := by
…
```

theorem OAI.LittleFinitistic.PDSquareZero.comap_jacobson line 29

Source documentation

A surjection with square-zero kernel pulls back the ring radical exactly.

theorem comap_jacobson (f : A →+* D) (hf : Function.Surjective f)
    (hsq : ∀ a ∈ RingHom.ker f, ∀ b ∈ RingHom.ker f, a*b=0) :
    Ideal.comap f (Ring.jacobson D) = Ring.jacobson A := by
…

theorem OAI.LittleFinitistic.PDSquareZero.kernel_square_zero line 42

Source documentation

The manuscript's actual split square-zero projection has square-zero kernel.

theorem kernel_square_zero (a b : TrivSqZeroExt D X)
    (ha : a ∈ RingHom.ker (TrivSqZeroExt.fstHom k D X).toRingHom)
    (hb : b ∈ RingHom.ker (TrivSqZeroExt.fstHom k D X).toRingHom) : a*b=0 := by
…

theorem OAI.LittleFinitistic.PDSquareZero.radical_eq_comap line 51
Source documentation
rad(D ⋉ X) is the preimage of rad(D), hence consists precisely of pairs whose D coordinate is in rad(D). The X coordinate is unrestricted.
```
theorem radical_eq_comap :
    Ring.jacobson (TrivSqZeroExt D X) =
      Ideal.comap (TrivSqZeroExt.fstHom k D X).toRingHom (Ring.jacobson D) := by
…
```
theorem OAI.LittleFinitistic.PDSquareZero.square_zero_ideal_le_radical line 61
Source documentation
Every simple A-module is annihilated by the square-zero ideal, as used when identifying the simple modules with those over D.
```
theorem square_zero_ideal_le_radical :
    RingHom.ker (TrivSqZeroExt.fstHom k D X).toRingHom ≤ Ring.jacobson (TrivSqZeroExt D X) :=
…
```