Base change along a decomposition by idempotents

A complete orthogonal family of idempotents f i of a commutative ring T decomposes T into the product of its components T ⧸ (1 - f i) (CompleteOrthogonalIdempotents.bijective_pi). Tensoring with a T-algebra X splits X accordingly into the product of its base changes to the components (CompleteOrthogonalIdempotents.tensorProductEquiv). Hence properties of X that are compatible with finite products and with restriction of scalars along T → T ⧸ (1 - f i) can be checked on each component; this file records it for module finiteness (TauCeti.Module.Finite.of_completeOrthogonalIdempotents).

Main declarations

• CompleteOrthogonalIdempotents.tensorProductEquiv: the splitting X ≃ₐ[T] Π i, (T ⧸ (1 - f i)) ⊗[T] X.
• TauCeti.Module.Finite.of_completeOrthogonalIdempotents: a module is finite if its base change to every component is.

noncomputable def CompleteOrthogonalIdempotents.tensorProductEquiv {T : Type u_1} [CommRing T] {ι : Type u_2} [Fintype ι] {f : ι → T} (hf : CompleteOrthogonalIdempotents f) (X : Type u_3) [Semiring X] [Algebra T X] : X ≃ₐ[T] (i : ι) → TensorProduct T (T ⧸ Ideal.span {1 - f i}) X

A complete orthogonal family of idempotents f i of T splits every T-algebra X into the product of its base changes to the components T ⧸ (1 - f i).

@[simp]

theorem CompleteOrthogonalIdempotents.tensorProductEquiv_apply {T : Type u_1} [CommRing T] {ι : Type u_2} [Fintype ι] {f : ι → T} (hf : CompleteOrthogonalIdempotents f) {X : Type u_3} [Semiring X] [Algebra T X] (x : X) (i : ι) : (hf.tensorProductEquiv X) x i = 1 ⊗ₜ[T] x

Each component of the splitting sends x to 1 ⊗ₜ x.

theorem TauCeti.Module.Finite.of_completeOrthogonalIdempotents {T : Type u_1} [CommRing T] {M : Type u_2} [AddCommMonoid M] [Module T M] {ι : Type u_3} [Fintype ι] {f : ι → T} (hf : CompleteOrthogonalIdempotents f) (h : ∀ (i : ι), Module.Finite (T ⧸ Ideal.span {1 - f i}) (TensorProduct T (T ⧸ Ideal.span {1 - f i}) M)) : Module.Finite T M

Module finiteness is local for a decomposition of the base by complete orthogonal idempotents: if the base change of M to every component T ⧸ (1 - f i) is finite, then M is finite over T.