fromQuotient — Mathlib

English

The map from the quotient to M is injective if and only if ker π equals the span of the relation images.

Русский

Отображение из фактор-модуля в M инъективно тогда и только тогда, когда ядро π равно оболочке образов отношений.

LaTeX

$$\text{Injective}(\text{solution.fromQuotient}) \ = \ (\ker(\text{solution.π}) = \operatorname{span}_A(\mathrm{Set.range}(\text{relations.relation})))$$

Lean4

/-- Given `relations : Relations A` and `solution : relations.Solution M`, this is
the canonical linear map `relations.Quotient →ₗ[A] M` from the module. -/
noncomputable def fromQuotient : relations.Quotient →ₗ[A] M :=
  Submodule.liftQ _ solution.π solution.span_relation_le_ker_π

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