English
Reiteration for coroot: the infimum of kernels equals the coroot span’s dual coannihilator.
Русский
Повторение для корорта: пересечение ядер равно двойственному коаннигилятивному охвату корорта.
LaTeX
$$⨅ i, ker(P.coroot' i) = (span R (range P.coroot')).dualCoannihilator$$
Lean4
/-- The coroot attached to a reflective vector. -/
def coroot : M →ₗ[R] R where
toFun y := (hx.2 y).choose
map_add' a
b := by
refine hx.1.1 ?_
simp only
rw [← (hx.2 (a + b)).choose_spec, mul_add, ← (hx.2 a).choose_spec, ← (hx.2 b).choose_spec, map_add, mul_add]
map_smul' r
a := by
refine hx.1.1 ?_
simp only [RingHom.id_apply]
rw [← (hx.2 (r • a)).choose_spec, smul_eq_mul, mul_left_comm, ← (hx.2 a).choose_spec, map_smul, two_mul,
smul_eq_mul, two_mul, mul_add]
