surjective_hom₁ — Mathlib

English

The map hom₁ is surjective onto the cotangent extension, achieved by supplying preimages for generators via the presentation.

Русский

Отображение hom₁ сюръективно на касательную расширения, задавая прообразы для генераторов через презентацию.

LaTeX

$$surjective_hom₁ pres$$

Lean4

theorem surjective_hom₁ : Function.Surjective (hom₁ pres) :=
  by
  let φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent :=
    { toFun := hom₁ pres
      map_add' := by simp
      map_smul' := by simp }
  change Function.Surjective φ
  have h₁ := Algebra.Extension.Cotangent.mk_surjective (P := pres.toExtension)
  have h₂ : Submodule.span pres.Ring (Set.range (fun r ↦ (⟨pres.relation r, by simp⟩ : pres.ker))) = ⊤ :=
    by
    refine Submodule.map_injective_of_injective (f := Submodule.subtype pres.ker) Subtype.coe_injective ?_
    rw [Submodule.map_top, Submodule.range_subtype, Submodule.map_span, Submodule.coe_subtype, Ideal.submodule_span_eq]
    simp only [← pres.span_range_relation_eq_ker]
    congr
    aesop
  rw [← LinearMap.range_eq_top] at h₁ ⊢
  rw [← top_le_iff, ← h₁, LinearMap.range_eq_map, ← h₂]
  dsimp
  rw [Submodule.map_span_le]
  rintro _ ⟨r, rfl⟩
  simp only [LinearMap.mem_range]
  refine ⟨Finsupp.single r 1, ?_⟩
  simp only [LinearMap.coe_mk, AddHom.coe_mk, hom₁_single, φ]
  rfl

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