English
There is a canonical linear isomorphism (over T) between the cotangent space of the composed map Q.comp P and the product of the cotangent space of Q and the T-tensor of P’s cotangent space: (Q.comp P).toExtension.CotangentSpace ≃_l[T] Q.toExtension.CotangentSpace × (T ⊗_S P.toExtension.CotangentSpace).
Русский
Существует каноническое линейное изоморфное отображение над T между котантной пространством композиции Q и P и произведением котантных пространств Q и T ⊗_S P: (Q.comp P).toExtension.CotangentSpace ≃_l[T] Q.toExtension.CotangentSpace × (T ⊗_S P.toExtension.CotangentSpace).
LaTeX
$$$$ (Q.comp P).toExtension.CotangentSpace \cong_T Q.toExtension.CotangentSpace \times (T \otimes_S P.toExtension.CotangentSpace). $$$$
Lean4
theorem exact :
Function.Exact ((Extension.Cotangent.map (Q.toComp P).toExtensionHom).liftBaseChange T)
(Extension.Cotangent.map (Q.ofComp P).toExtensionHom) :=
by
apply LinearMap.exact_of_comp_of_mem_range
· rw [LinearMap.liftBaseChange_comp, ← Extension.Cotangent.map_comp, EmbeddingLike.map_eq_zero_iff]
ext x
obtain ⟨⟨x, hx⟩, rfl⟩ := Extension.Cotangent.mk_surjective x
simp only [map_mk, val_mk, LinearMap.zero_apply, val_zero]
convert Q.ker.toCotangent.map_zero
trans ((IsScalarTower.toAlgHom R _ _).comp (IsScalarTower.toAlgHom R P.Ring S)) x
· congr
refine MvPolynomial.algHom_ext fun i ↦ ?_
change (Q.ofComp P).toAlgHom ((Q.toComp P).toAlgHom (X i)) = _
simp
· simp [aeval_val_eq_zero hx]
· intro x hx
obtain ⟨⟨x : (Q.comp P).Ring, hx'⟩, rfl⟩ := Extension.Cotangent.mk_surjective x
replace hx : (Q.ofComp P).toAlgHom x ∈ Q.ker ^ 2 := by
simpa only [map_mk, val_mk, val_zero, Ideal.toCotangent_eq_zero] using congr(($hx).val)
rw [pow_two, ← map_ofComp_ker (P := P), ← Ideal.map_mul,
Ideal.mem_map_iff_of_surjective _ (toAlgHom_ofComp_surjective Q P)] at hx
obtain ⟨y, hy, e⟩ := hx
rw [eq_comm, ← sub_eq_zero, ← map_sub, ← RingHom.mem_ker, ← map_toComp_ker] at e
rw [LinearMap.range_liftBaseChange]
let z : (Q.comp P).ker := ⟨x - y, Ideal.sub_mem _ hx' (Ideal.mul_le_left hy)⟩
have hz : z.1 ∈ P.ker.map (Q.toComp P).toAlgHom.toRingHom := e
have : Extension.Cotangent.mk (P := (Q.comp P).toExtension) ⟨x, hx'⟩ = Extension.Cotangent.mk z := by ext;
simpa only [val_mk, Ideal.toCotangent_eq, sub_sub_cancel, pow_two, z]
rw [this, ← Submodule.restrictScalars_mem (Q.comp P).Ring, ← Submodule.mem_comap, ←
Submodule.span_singleton_le_iff_mem, ←
Submodule.map_le_map_iff_of_injective (f := Submodule.subtype _) Subtype.val_injective,
Submodule.map_subtype_span_singleton, Submodule.span_singleton_le_iff_mem]
refine (show Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker ≤ _ from ?_) hz
rw [Ideal.map_le_iff_le_comap]
rintro w hw
simp only [AlgHom.toRingHom_eq_coe, Ideal.mem_comap, RingHom.coe_coe, Submodule.mem_map, Submodule.mem_comap,
Submodule.restrictScalars_mem, Submodule.coe_subtype, Subtype.exists, exists_and_right, exists_eq_right,
toExtension_Ring, toExtension_commRing, toExtension_algebra₂]
refine ⟨?_, Submodule.subset_span ⟨Extension.Cotangent.mk ⟨w, hw⟩, ?_⟩⟩
· simp only [ker_eq_ker_aeval_val, RingHom.mem_ker, Hom.algebraMap_toAlgHom]
rw [aeval_val_eq_zero hw, map_zero]
· rw [map_mk]
rfl
