English
For finite σ, the map cotangentComplexAux associated to a PreSubmersivePresentation P is injective.
Русский
Для конечного σ отображение cotangentComplexAux, связанное с пред-subмёрсивным представлением P, инъективно.
LaTeX
$$For finite σ, \(P.cotangentComplexAux\) is injective.$$
Lean4
theorem cotangentComplexAux_injective [Finite σ] : Function.Injective P.cotangentComplexAux :=
by
rw [← LinearMap.ker_eq_bot, eq_bot_iff]
intro x hx
obtain ⟨(x : P.ker), rfl⟩ := Cotangent.mk_surjective x
rw [Submodule.mem_bot, Cotangent.mk_eq_zero_iff]
rw [LinearMap.mem_ker, P.cotangentComplexAux_zero_iff] at hx
have : x.val ∈ Ideal.span (Set.range P.relation) :=
by
rw [P.span_range_relation_eq_ker]
exact x.property
obtain ⟨c, hc⟩ := Finsupp.mem_ideal_span_range_iff_exists_finsupp.mp this
have heq (i : σ) : aeval P.val (pderiv (P.map i) <| c.sum fun i a ↦ a * P.relation i) = 0 :=
by
rw [hc]
apply hx
simp only [Finsupp.sum, map_sum, Derivation.leibniz, smul_eq_mul, map_add, map_mul, Presentation.aeval_val_relation,
zero_mul, add_zero] at heq
have heq2 : ∑ i ∈ c.support, aeval P.val (c i) • (fun j ↦ aeval P.val (pderiv (P.map j) (P.relation i))) = 0 :=
by
ext j
simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Pi.zero_apply]
apply heq
have (i : σ) : aeval P.val (c i) = 0 :=
by
have := P.linearIndependent_aeval_val_pderiv_relation
rw [linearIndependent_iff''] at this
have :=
this c.support (fun i ↦ aeval P.val (c i))
(by intro i; simp only [Finsupp.mem_support_iff, ne_eq, not_not]; intro h; simp [h]) heq2
exact this i
change _ ∈ P.ker ^ 2
rw [← hc]
apply Ideal.sum_mem
intro i hi
rw [pow_two]
apply Ideal.mul_mem_mul
· rw [P.ker_eq_ker_aeval_val]
simpa using this i
· exact P.relation_mem_ker i
