Independent families of submodules and traces #
The traces (I i).comap S.subtype of an independent family of submodules I on a submodule S
are independent (iSupIndep.comap_subtype).
theorem
iSupIndep.comap_subtype
{R : Type u_1}
{M : Type u_2}
{ι : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Submodule R M}
{I : ι → Submodule R M}
(hI : iSupIndep I)
:
iSupIndep fun (i : ι) => Submodule.comap S.subtype (I i)
The traces of an independent family of submodules on a submodule S are independent.