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