algebraRight — Mathlib

English

Define λ on IncidenceAlgebra 𝕜 α by λ(a,b) = 1 if a ⩿ b and the interval [a,b] is nonempty with cardinality 1 or 2, and λ(a,b) = 0 otherwise; this λ is an element of the incidence algebra (the lambda function).

Русский

Задаём λ на IncidenceAlgebra 𝕜 α так, что λ(a,b) = 1, если a ⩿ b и интервал [a,b] непустой и имеет нумерацию 1 или 2, иначе λ(a,b) = 0; это элемент инцидентальной алгебры.

LaTeX

$$$ \lambda(a,b) = \begin{cases} 1, & a \mathrel{⩿} b, \\ 0, & \text{иначе} \end{cases}$$$

Lean4

instance algebraRight [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] [CommSemiring 𝕜] [CommSemiring 𝕝]
    [Algebra 𝕜 𝕝] : Algebra 𝕜 (IncidenceAlgebra 𝕝 α)
    where
  algebraMap :=
    { toFun c := algebraMap 𝕜 𝕝 c • (1 : IncidenceAlgebra 𝕝 α)
      map_one' := by ext; simp only [mul_boole, one_apply, Algebra.id.smul_eq_mul, constSMul_apply, map_one]
      map_mul' c
        d := by
        ext a b
        obtain rfl | h := eq_or_ne a b
        · simp only [one_apply, Algebra.id.smul_eq_mul, mul_apply, constSMul_apply, map_mul, eq_comm, Icc_self]
          simp
        · simp only [one_apply, mul_one, Algebra.id.smul_eq_mul, mul_apply, zero_mul, constSMul_apply, ← ite_and,
            ite_mul, mul_ite, map_mul, mul_zero, if_neg h]
          refine (sum_eq_zero fun x _ ↦ ?_).symm
          exact if_neg fun hx ↦ h <| hx.2.trans hx.1
      map_zero' := by rw [map_zero, zero_smul]
      map_add' c d := by rw [map_add, add_smul] }
  commutes' c f := by classical ext a b hab; simp [if_pos hab, constSMul_apply, mul_comm]
  smul_def' c f := by classical ext a b hab; simp [if_pos hab, constSMul_apply, Algebra.smul_def]

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