AlgHom.existsUnique_lift_trivSqZeroExt_of_cotangent_linearMap
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AlgHom_existsUnique_lift_trivSqZeroExt_of_cotangent_linearMap
universe u v xLean source · statement
theorem _root_.AlgHom.existsUnique_lift_trivSqZeroExt_of_cotangent_linearMap
{𝒪 : Type u} [CommRing 𝒪] {R : Type v} [CommRing R] [Algebra 𝒪 R] (πR : R →ₐ[𝒪] 𝒪)
{N : Type x} [AddCommGroup N] [Module 𝒪 N] [Module 𝒪ᵐᵒᵖ N] [IsCentralScalar 𝒪 N]
(f : (RingHom.ker πR).Cotangent →ₗ[𝒪] N) :
∃! ψ : R →ₐ[𝒪] TrivSqZeroExt 𝒪 N, (∀ r : R, (ψ r).fst = πR r) ∧
∀ a : RingHom.ker πR, (ψ (a : R)).snd = f ((RingHom.ker πR).toCotangent a)