PDRadical.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.PDRadical.jacobson_eq_smul line 15
Source documentation
For a finitely generated projective module the module radical is exactly multiplication by the ring Jacobson radical. No commutativity is assumed.
```
theorem jacobson_eq_smul [Module.Finite A P] [Module.Projective A P] :
    Module.jacobson A P = Ring.jacobson A • (⊤ : Submodule A P) := by
…
```

theorem OAI.LittleFinitistic.PDRadical.quotient_radical_nontrivial line 44

Source documentation

The noncommutative Nakayama step used in the manuscript.

theorem quotient_radical_nontrivial [Module.Finite A P] [Nontrivial P] :
    Nontrivial (P ⧸ (Ring.jacobson A • (⊤ : Submodule A P))) := by
…

theorem OAI.LittleFinitistic.PDRadical.simple_map_radical_zero line 50

Source documentation

Any map into a simple module annihilates the radical of its domain.

theorem simple_map_radical_zero
    {S : Type v} [AddCommGroup S] [Module A S] [IsSimpleModule A S]
    (f : P →ₗ[A] S) (x : P) (hx : x ∈ Module.jacobson A P) : f x = 0 := by
…