Theorems · Theorem · linear algebra

Module.pi_induction

∀ (R : Type u) [inst : Semiring R] {ι : Type v} [Finite ι]
  (motive : (N : Type u) → [inst_2 : AddCommMonoid N] → [Module R N] → Prop)
  (motive' : (N : Type (max u v)) → [inst_2 : AddCommMonoid N] → [Module R N] → Prop),
  (∀ {N : Type u} {N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
      [inst_5 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N') →
    (∀ {N N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
        [inst_5 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N') →
      motive PUnit.{u + 1} →
        (∀ {N : Type u} {N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N']
            [inst_4 : Module R N] [inst_5 : Module R N'], motive N → motive' N' → motive' (N × N')) →
          ∀ (M : ι → Type u) [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R (M i)],
            (∀ (i : ι), motive (M i)) → motive' ((i : ι) → M i)

To show a property motive of modules holds for arbitrary finite products of modules, it suffices to show 1. motive is stable under isomorphism. 2. motive holds for the zero module. 3. motive holds for M × N if it holds for both M and N. Since we need to apply motive to modules in Type u and in Type (max u v), there is a second motive' argument which is required to be equivalent to motive up to universe lifting by equiv. See Module.pi_induction' for a version where motive assumes AddCommGroup instead.

Defined in

Mathlib.LinearAlgebra.Pi

Cited by

0 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringFiniteAddCommMonoidModule