right_induction — Mathlib

English

Consider the auxiliary construction foldr'Aux Q f. It encodes a bilinear action that, when iterated on an input v and a pair (m, x), yields a pair whose first component is the product of ι_Q m and x in Clifford direction and whose second component tracks f m x. The fold over this auxiliary step matches Q-weighted action on x.

Русский

Рассматривается вспомогательная конструкция foldr'Aux, которая кодирует билинейное действие; повторная свёртка по ней даёт пару, где первый элемент — произведение ι_Q m и x, а второй — отслеживает f m x; свёртка по этой схеме даёт действие, взвешенное весом Q.

LaTeX

$$$foldr'Aux\\ Q\\ f\\ v\\ x_{fx} = (ι_Qm \\cdot x, f m x_fx)$$$

Lean4

@[elab_as_elim]
theorem right_induction {P : CliffordAlgebra Q → Prop} (algebraMap : ∀ r : R, P (algebraMap _ _ r))
    (add : ∀ x y, P x → P y → P (x + y)) (mul_ι : ∀ m x, P x → P (x * ι Q m)) : ∀ x, P x := by
  /- It would be neat if we could prove this via `foldr` like how we prove
      `CliffordAlgebra.induction`, but going via the grading seems easier. -/

  intro x
  have : x ∈ ⊤ := Submodule.mem_top (R := R)
  rw [← iSup_ι_range_eq_top] at this
  induction this using Submodule.iSup_induction' with
  | mem i x hx =>
    induction hx using Submodule.pow_induction_on_right' with
    | algebraMap r => exact algebraMap r
    | add _x _y _i _ _ ihx ihy => exact add _ _ ihx ihy
    | mul_mem _i x _hx px m hm =>
      obtain ⟨m, rfl⟩ := hm
      exact mul_ι _ _ px
  | zero => simpa only [map_zero] using algebraMap 0
  | add _x _y _ _ ihx ihy => exact add _ _ ihx ihy

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