mem_span_fractionalIdealLatticeBasis

English

The span over Z of the fractionalIdealLatticeBasis equals the image of the fractional ideal under mixedEmbedding.

Русский

Замыкание по целым числам fractI вычисляет образ дробного идеала через смешанное вложение.

LaTeX

$$$ x \in Submodule.span \mathbb{Z} (Set.range (fractionalIdealLatticeBasis K I)) \Leftrightarrow x \in mixedEmbedding K '' I $$$

Lean4

theorem mem_span_fractionalIdealLatticeBasis {x : (mixedSpace K)} :
    x ∈ Submodule.span ℤ (Set.range (fractionalIdealLatticeBasis K I)) ↔ x ∈ mixedEmbedding K '' I :=
  by
  rw [show
      Set.range (fractionalIdealLatticeBasis K I) =
        (mixedEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (basisOfFractionalIdeal K I))
      by
      rw [← Set.range_comp]
      exact congr_arg Set.range (funext (fun i ↦ fractionalIdealLatticeBasis_apply K I i))]
  rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe]
  rw [show Submodule.span ℤ (Set.range (basisOfFractionalIdeal K I)) = (I : Set K) by ext;
      simp [mem_span_basisOfFractionalIdeal]]
  rfl

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