Smallness properties of modules and algebras

instance Submodule.small_sup {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {P Q : Submodule R M} [smallP : Small.{u, u_2} ↥P] [smallQ : Small.{u, u_2} ↥Q] : Small.{u, u_2} ↥(P ⊔ Q)

instance Submodule.instSemilatticeSupSubtypeSmallMem {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] : SemilatticeSup { P : Submodule R M // Small.{u, u_2} ↥P }

Equations

• Submodule.instSemilatticeSupSubtypeSmallMem = SemilatticeSup.mk (fun (P Q : { P : Submodule R M // Small.{?u.43, ?u.41} ↥P }) => ⟨↑P ⊔ ↑Q, ⋯⟩) ⋯ ⋯ ⋯

instance Submodule.instInhabitedSubtypeSmallMem {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] : Inhabited { P : Submodule R M // Small.{u, u_2} ↥P }

Equations

• Submodule.instInhabitedSubtypeSmallMem = { default := ⟨⊥, ⋯⟩ }

instance Submodule.small_iSup {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {P : ι → Submodule R M} [Small.{u, u_3} ι] [∀ (i : ι), Small.{u, u_2} ↥(P i)] : Small.{u, u_2} ↥(iSup P)

theorem Submodule.FG.small {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Small.{u, u_1} R] (P : Submodule R M) (hP : P.FG) : Small.{u, u_2} ↥P

theorem Module.Finite.small (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Small.{u, u_1} R] [Module.Finite R M] : Small.{u, u_2} M

instance Submodule.small_span_singleton {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Small.{u, u_1} R] (m : M) : Small.{u, u_2} ↥(span R {m})

theorem Submodule.small_span {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Small.{u, u_1} R] (s : Set M) [Small.{u, u_2} ↑s] : Small.{u, u_2} ↥(span R s)

instance Algebra.small_adjoin {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] [Small.{u, u_1} R] {s : Set S} [Small.{u, u_2} ↑s] : Small.{u, u_2} ↥(adjoin R s)

theorem Subalgebra.FG.small {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] [Small.{u, u_1} R] {A : Subalgebra R S} (fgS : A.FG) : Small.{u, u_2} ↥A

theorem Algebra.FiniteType.small {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] [Small.{u, u_1} R] [FiniteType R S] : Small.{u, u_2} S