Stably free modules

Main definition

• IsStablyFree: A module M over a commutative ring R is called stably free if there exists a finite free module N over R such that M ⊕ N is free.

class Module.IsStablyFree (R : Type u) [Ring R] (M : Type u_1) [AddCommGroup M] [Module R M] : Prop

A module M over a commutative ring R is called stably free if there exists a finite free module N over R such that M ⊕ N is free.

The underlying constructor is marked as private. The intended constructor of IsStablyFree is IsStablyFree.of_free_prod, and use IsStablyFree.exist_free_prod to extract the property from IsStablyFree.

• exist_free_prod' : ∃ (N : Type u) (x : AddCommGroup N) (x_1 : Module R N) (_ : Module.Finite R N) (_ : Module.Free R N), Module.Free R (M × N)

theorem Module.IsStablyFree.exist_free_prod (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [IsStablyFree R M] : ∃ (N : Type u) (x : AddCommGroup N) (x_1 : Module R N) (_ : Module.Finite R N) (_ : Free R N), Free R (M × N)

theorem Module.IsStablyFree.equiv {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) [IsStablyFree R M] : IsStablyFree R N

theorem Module.IsStablyFree.equiv_iff {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) : IsStablyFree R M ↔ IsStablyFree R N

instance Module.IsStablyFree.ulift (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [IsStablyFree R M] : IsStablyFree R (ULift.{w, v} M)

theorem Module.IsStablyFree.of_ulift (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [IsStablyFree R (ULift.{w, v} M)] : IsStablyFree R M

instance Module.IsStablyFree.shrink (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [Small.{w, v} M] [IsStablyFree R M] : IsStablyFree R (Shrink.{w, v} M)

theorem Module.IsStablyFree.of_shrink (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [Small.{w, v} M] [IsStablyFree R (Shrink.{w, v} M)] : IsStablyFree R M

instance Module.instIsStablyFreeOfFree (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [Free R M] : IsStablyFree R M

theorem Module.IsStablyFree.of_free_prod (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] (N : Type w) [AddCommGroup N] [Module R N] [Module.Finite R N] [Free R N] [Free R (M × N)] : IsStablyFree R M

theorem Module.IsStablyFree.of_free_prod' (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] (N : Type w) [AddCommGroup N] [Module R N] [Module.Finite R N] [Free R N] [Free R (N × M)] : IsStablyFree R M

@[instance 100]

instance Module.instProjectiveOfIsStablyFree (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [IsStablyFree R M] : Projective R M