range_mapBaseChange — Mathlib

English

The range of mapBaseChange equals the kernel of map under the base change, restricted to A.

Русский

Образ mapBaseChange равен ядру map под базовым изменением, ограниченному до A.

LaTeX

$$$\\mathrm{range}(\\mathrm{mapBaseChange}\\,R\\,A\\,B) = \\mathrm{ker}(\\mathrm{map}\\,R\\,A\\,B)\\restrictionScalars A$$$

Lean4

theorem range_mapBaseChange : LinearMap.range (mapBaseChange R A B) = LinearMap.ker (map R A B B) :=
  by
  apply le_antisymm
  · rintro _ ⟨x, rfl⟩
    induction x with
    | zero => simp
    | tmul r s =>
      obtain ⟨x, rfl⟩ := linearCombination_surjective _ _ s
      simp only [mapBaseChange_tmul, LinearMap.mem_ker, map_smul]
      induction x using Finsupp.induction_linear
      · simp
      · simp [smul_add, *]
      · simp
    | add => rw [map_add]; exact add_mem ‹_› ‹_›
  · convert_to (kerTotal A B).map (Finsupp.linearCombination B (D R B)) ≤ _
    · rw [KaehlerDifferential.ker_map]
      congr 1
      convert Submodule.comap_id _
      · ext; simp
    rw [Submodule.map_le_iff_le_comap, kerTotal, Submodule.span_le]
    rintro f ((⟨⟨x, y⟩, rfl⟩ | ⟨⟨x, y⟩, rfl⟩) | ⟨x, rfl⟩)
    · use 0; simp
    · use 0; simp
    · use 1 ⊗ₜ D _ _ x; simp

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