English
Given an embedding r: ι ↪ M and a family c of Duals with f i x = 2 for all i, and MapsTo preReflection (r i) (c i) on range r, the map from span R (range r).subtype.dualMap to range c is injective.
Русский
Пусть имеется вложение r: ι ↪ M и семейство c из двойственных линейных форм так, что f_i(r_i)=2 для всех i, и отображения preReflection сохраняют диапазон; тогда отображение из span R (range r).subtype.dualMap в range c инъективно.
LaTeX
$$$\\text{Let } r:ι\\hookrightarrow M,\\ c:ι→M^*,\\text{ with } c i (r i)=2,\\text{ and } MapsTo(\\mathrm{preReflection}(r i,c i),\\mathrm{range}(r),\\mathrm{range}(r))\\text{ for all i. Then }\\ InjOn\\; (span R(\\mathrm{range}\\;r)).subtype.dualMap(\\mathrm{range}\\;c).$$$
Lean4
theorem injOn_dualMap_subtype_span_range_range {ι : Type*} [NoZeroSMulDivisors ℤ M] {r : ι ↪ M} {c : ι → Dual R M}
(hfin : (range r).Finite) (h_two : ∀ i, c i (r i) = 2)
(h_mapsTo : ∀ i, MapsTo (preReflection (r i) (c i)) (range r) (range r)) :
InjOn (span R (range r)).subtype.dualMap (range c) :=
by
rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩ hij
congr
suffices ∀ k, c i (r k) = c j (r k) by
rw [← EmbeddingLike.apply_eq_iff_eq r]
exact
eq_of_mapsTo_reflection_of_mem (f := c i) (g := c j) hfin (h_two i) (h_two j) (by rw [← this, h_two])
(by rw [this, h_two]) (h_mapsTo i) (h_mapsTo j) (mem_range_self j)
intro k
simpa using LinearMap.congr_fun hij ⟨r k, Submodule.subset_span (mem_range_self k)⟩
