comap — Mathlib

English

Pulling back along the identity linear map yields the original lattice: ZLattice.comap K L id = L.

Русский

Возврат через тождественный линейный преобразователь даёт исходную решётку: ZLattice.comap K L id = L.

LaTeX

$$$ZLattice.comap K L (1:E\\to E) = L$$$

Lean4

/-- Let `e : E → F` a linear map, the map that sends a `L : Submodule ℤ E` to the
`Submodule ℤ F` that is the pullback of `L` by `e`. If `IsZLattice L` and `e` is a continuous
linear equiv, then it is a `IsZLattice` of `E`, see `instIsZLatticeComap`. -/
protected def comap (e : F →ₗ[K] E) :=
  L.comap (e.restrictScalars ℤ)

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