pi_induction — Mathlib

English

The linear map vecEmpty : M →ₗ[R] Fin 0 → M₃ is defined by toFun(m) = Matrix.vecEmpty, and is linear by subsingleton arguments.

Русский

Линейное отображение vecEmpty: M →ₗ[R] Fin 0 → M₃ задаётся как toFun(m) = Matrix.vecEmpty и линейно потому что подмножество скаляется и суммируется тривиально.

LaTeX

$$$$ \\text{vecEmpty} : M \\to_{R} Fin(0) \\to M_3, \\quad \\text{toFun}(m) = \\text{Matrix.vecEmpty}, $$$$

Lean4

/-- 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.
-/
@[elab_as_elim]
theorem pi_induction {ι : Type v} [Finite ι] (motive : ∀ (N : Type u) [AddCommMonoid N] [Module R N], Prop)
    (motive' : ∀ (N : Type (max u v)) [AddCommMonoid N] [Module R N], Prop)
    (equiv :
      ∀ {N : Type u} {N' : Type (max u v)} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'],
        (N ≃ₗ[R] N') → motive N → motive' N')
    (equiv' :
      ∀ {N N' : Type (max u v)} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'],
        (N ≃ₗ[R] N') → motive' N → motive' N')
    (unit : motive PUnit)
    (prod :
      ∀ {N : Type u} {N' : Type (max u v)} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'],
        motive N → motive' N' → motive' (N × N'))
    (M : ι → Type u) [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)] (h : ∀ i, motive (M i)) : motive' (∀ i, M i) := by
  classical
  cases nonempty_fintype ι
  revert M
  refine
    Fintype.induction_empty_option (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
      (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
  exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)

Похожие утверждения