English
Equivalence: injectivity of the quotient-from-solution map is equivalent to ker π equaling the span of relation images.
Русский
Эквивалентность: инъективность перехода до фактор-модуля равна равенству кернела π оболочке образов отношений.
LaTeX
$$$\text{Injective}(\text{solution.fromQuotient}) \; \Longleftrightarrow \; \ker(\text{solution.π}) = \operatorname{span}_A(\mathrm{Set.range}(\text{relations.relation}))$$$
Lean4
theorem injective_fromQuotient_iff_ker_π_eq_span :
Function.Injective solution.fromQuotient ↔
LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation) :=
by
constructor
· intro h
rw [← ker_toQuotient, ← fromQuotient_comp_toQuotient, LinearMap.ker_comp, LinearMap.ker_eq_bot.2 h,
Submodule.comap_bot]
· intro h
rw [← LinearMap.ker_eq_bot, eq_bot_iff]
intro x hx
obtain ⟨x, rfl⟩ := relations.surjective_toQuotient x
replace hx : x ∈ LinearMap.ker solution.π := by simpa only [LinearMap.mem_ker, fromQuotient_toQuotient] using hx
rw [h, ← range_map] at hx
obtain ⟨x, rfl⟩ := hx
simp only [toQuotient_map_apply, Submodule.zero_mem]
