range_kerCotangentToTensor — Mathlib

English

The range of kerCotangentToTensor equals the ker of mapBaseChange after restricting scalars.

Русский

Образ kerCotangentToTensor равен ядру mapBaseChange после ограничения скалярного действия.

LaTeX

$$$\\mathrm{range}(\\kerCotangentToTensor\\,R\\,A\\,B) = (\\ker(\\mathrm{mapBaseChange}\\,R\\,A\\,B)).restrictScalars A$$$

Lean4

theorem range_kerCotangentToTensor (h : Function.Surjective (algebraMap A B)) :
    LinearMap.range (kerCotangentToTensor R A B) =
      (LinearMap.ker (KaehlerDifferential.mapBaseChange R A B)).restrictScalars A :=
  by
  classical
  ext x
  constructor
  · rintro ⟨x, rfl⟩
    obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x
    simp only [kerCotangentToTensor_toCotangent, Submodule.restrictScalars_mem, LinearMap.mem_ker, mapBaseChange_tmul,
      map_D, RingHom.mem_ker.mp x.2, map_zero, smul_zero]
  · intro hx
    obtain ⟨x, rfl⟩ := LinearMap.rTensor_surjective Ω[A⁄R] (g := Algebra.linearMap A B) h x
    obtain ⟨x, rfl⟩ := (TensorProduct.lid _ _).symm.surjective x
    replace hx : x ∈ LinearMap.ker (KaehlerDifferential.map R R A B) := by simpa using hx
    rw [KaehlerDifferential.ker_map_of_surjective R A B h] at hx
    obtain ⟨x, hx, rfl⟩ := hx
    simp only [TensorProduct.lid_symm_apply, LinearMap.rTensor_tmul, Algebra.linearMap_apply, map_one]
    rw [← Finsupp.sum_single x, Finsupp.sum, ←
      Finset.sum_fiberwise_of_maps_to (fun _ ↦ Finset.mem_image_of_mem (algebraMap A B))]
    simp only [map_sum (s := x.support.image (algebraMap A B)), TensorProduct.tmul_sum]
    apply sum_mem
    intro c _
    simp only [LinearMap.mem_range]
    simp only [map_sum, Finsupp.linearCombination_single]
    have : ∑ i ∈ x.support with algebraMap A B i = c, x i ∈ RingHom.ker (algebraMap A B) := by
      simpa [Finsupp.mapDomain, Finsupp.sum, Finsupp.finset_sum_apply, RingHom.mem_ker, Finsupp.single_apply,
        ← Finset.sum_filter] using DFunLike.congr_fun hx c
    obtain ⟨a, ha⟩ := h c
    use ∑ i ∈ {i ∈ x.support | algebraMap A B i = c}.attach, x i • Ideal.toCotangent _ ⟨i - a, ?_⟩
    · simp only [map_sum, LinearMapClass.map_smul, kerCotangentToTensor_toCotangent, map_sub]
      simp_rw [← TensorProduct.tmul_smul]
        -- TODO: was `simp [kerCotangentToTensor_toCotangent, RingHom.mem_ker.mp x.2]` and very slow
              -- (https://github.com/leanprover-community/mathlib4/issues/19751)

      simp only [smul_sub, TensorProduct.tmul_sub, Finset.sum_sub_distrib, ← TensorProduct.tmul_sum, ← Finset.sum_smul,
        Finset.sum_attach, sub_eq_self, Finset.sum_attach (f := fun i ↦ x i • KaehlerDifferential.D R A i)]
      rw [← TensorProduct.smul_tmul, ← Algebra.algebraMap_eq_smul_one, RingHom.mem_ker.mp this, TensorProduct.zero_tmul]
    · have : x i ≠ 0 ∧ algebraMap A B i = c := by
        convert i.prop
        simp_rw [Finset.mem_filter, Finsupp.mem_support_iff]
      simp [RingHom.mem_ker, ha, this.2]

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