PDCovers.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.PDCovers.RightMinimal line 16
Source documentation
An epimorphism is right minimal if every endomorphism over it is surjective.
```
def RightMinimal (p : E →ₗ[A] N) : Prop :=
…
```
lemma OAI.LittleFinitistic.PDCovers.comp_pow_eq line 19

theorem OAI.LittleFinitistic.PDCovers.rightMinimal_of_minimal line 27

Source documentation

Fitting decomposition upgrades minimality among projective submodules to right minimality of an actual epimorphism.

theorem rightMinimal_of_minimal [IsArtinian A E] [IsNoetherian A E]
    (p : E →ₗ[A] N) (S : Submodule A E)
    (hS : Minimal (fun T : Submodule A E =>
      Module.Projective A T ∧ Function.Surjective (p.comp T.subtype)) S) :
    RightMinimal (p.comp S.subtype) := by
…

Mentions: OAI.LittleFinitistic.PDCovers.RightMinimal

theorem OAI.LittleFinitistic.PDCovers.exists_rightMinimal line 69

Source documentation

Every projective epimorphism from a finite-length module contains a projective cover. This proves existence rather than assuming covers.

theorem exists_rightMinimal [IsArtinian A E] [IsNoetherian A E]
    [Module.Projective A E] (p : E →ₗ[A] N) (hp : Function.Surjective p) :
    ∃ S : Submodule A E, Module.Projective A S ∧
      Function.Surjective (p.comp S.subtype) ∧ RightMinimal (p.comp S.subtype) := by
…

Mentions: OAI.LittleFinitistic.PDCovers.RightMinimal