PDCoverRadical.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.PDCovers.eq_top_of_sup_ker line 15

Source documentation

A projective right-minimal epimorphism has a superfluous kernel.

theorem eq_top_of_sup_ker [Module.Projective A E]
    (p : E →ₗ[A] N) (hp : Function.Surjective p) (hm : RightMinimal p)
    (L : Submodule A E) (hL : L ⊔ LinearMap.ker p = ⊤) : L = ⊤ := by
…

Mentions: OAI.LittleFinitistic.PDCovers.RightMinimal

theorem OAI.LittleFinitistic.PDCovers.ker_le_jacobson line 37
Source documentation
Projective-cover kernels lie in the actual module Jacobson radical.
```
theorem ker_le_jacobson [Module.Projective A E]
    (p : E →ₗ[A] N) (hp : Function.Surjective p) (hm : RightMinimal p) :
    LinearMap.ker p ≤ Module.jacobson A E := by
…
```
Mentions: OAI.LittleFinitistic.PDCovers.RightMinimal

theorem OAI.LittleFinitistic.PDCovers.exists_finite_projective_cover line 49

Source documentation

Over a finite-dimensional algebra every finite-dimensional module has an actual finitely generated projective cover, constructed inside a finite free module.

theorem exists_finite_projective_cover
    {k : Type u} [Field k] [Algebra k A] [FiniteDimensional k A]
    [Module k N] [IsScalarTower k A N] [FiniteDimensional k N] :
    ∃ (n : ℕ) (S : Submodule A (Fin n → A)) (p : S →ₗ[A] N),
      Module.Projective A S ∧ Function.Surjective p ∧
      RightMinimal p ∧ LinearMap.ker p ≤ Module.jacobson A S := by
…

Mentions: OAI.LittleFinitistic.PDCovers.RightMinimal