English
If e is a linear equivalence, then there is a ℤ-linear equivalence between L and ZLattice.comap K L e.
Русский
Если e — линейное эквивалентность, существует ℤ-линейное эквивалентное отображение между L и ZLattice.comap K L e.
LaTeX
$$$L \\cong_{\\mathbb{Z}} ZLattice.comap K L e$$$
Lean4
/-- If `e` is a linear equivalence, it induces a `ℤ`-linear equivalence between
`L` and `ZLattice.comap K L e`. -/
def comap_equiv (e : F ≃ₗ[K] E) : L ≃ₗ[ℤ] (ZLattice.comap K L e.toLinearMap) :=
LinearEquiv.ofBijective
((e.symm.toLinearMap.restrictScalars ℤ).restrict (fun _ h ↦ by simpa [← SetLike.mem_coe] using h))
⟨fun _ _ h ↦ Subtype.ext_iff.mpr (e.symm.injective (congr_arg Subtype.val h)), fun ⟨x, hx⟩ ↦
⟨⟨e x, by rwa [← SetLike.mem_coe, ZLattice.coe_comap] at hx⟩, by simp [Subtype.ext_iff]⟩⟩
