English
For generators Q of S→T and P of R→S with the appropriate scalar-tower hypotheses, the cotangent-space map Extensions.Cotangent.map from (Q.ofComp P) toExtensionHom is surjective.
Русский
Для генераторов Q: S→T и P: R→S при наличии соответствующих условий тензорной башни, отображение котант-сопровождающее extension map из (Q.ofComp P) в toExtensionHom сюръективно.
LaTeX
$$$$\forall y \in \mathrm{ExtCotangentSpace}( (Q.ofComp P).toExtensionHom ), \exists x: \mathrm{ExtCotangentSpace}( (Q.ofComp P).toExtensionHom )\; \mathrm{ such that } \mathrm{Extension.Cotangent}.map( (Q.ofComp P).toExtensionHom )(x) = y.$$$$
Lean4
theorem surjective_map_ofComp : Function.Surjective (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) :=
by
intro x
obtain ⟨⟨x, hx⟩, rfl⟩ := Extension.Cotangent.mk_surjective x
have : x ∈ Q.ker := hx
rw [← map_ofComp_ker Q P, Ideal.mem_map_iff_of_surjective _ (toAlgHom_ofComp_surjective Q P)] at this
obtain ⟨x, hx', rfl⟩ := this
exact ⟨.mk ⟨x, hx'⟩, Extension.Cotangent.map_mk _ _⟩
