pi_induction' — Mathlib

English

A bilinear construction vecCons₂ builds a map into Fin(n+1) from two maps into M₂ and Fin(n) by appending a new coordinate.

Русский

Построение vecCons₂ добавляет координату к существующим двум линейным отображениям, образуя отображение в Fin(n+1).

LaTeX

$$$\\text{vecCons₂} : (M \\rightarrow M_2 \\rightarrow M_3) \\rightarrow (M \\rightarrow M_2 \\rightarrow (\\mathrm{Fin}\\; n \\rightarrow M_3)) \\rightarrow (M \\rightarrow M_2 \\rightarrow (\\mathrm{Fin}\\; (n+1) \\rightarrow M_3)).$$$

Lean4

/-- A variant of `Module.pi_induction` that assumes `AddCommGroup` instead of `AddCommMonoid`. -/
@[elab_as_elim]
theorem pi_induction' {ι : Type v} [Finite ι] (R : Type*) [Ring R]
    (motive : ∀ (N : Type u) [AddCommGroup N] [Module R N], Prop)
    (motive' : ∀ (N : Type (max u v)) [AddCommGroup N] [Module R N], Prop)
    (equiv :
      ∀ {N : Type u} {N' : Type (max u v)} [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N'],
        (N ≃ₗ[R] N') → motive N → motive' N')
    (equiv' :
      ∀ {N N' : Type (max u v)} [AddCommGroup N] [AddCommGroup 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)} [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N'],
        motive N → motive' N' → motive' (N × N'))
    (M : ι → Type u) [∀ i, AddCommGroup (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)

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