NYLL
Module

Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
42 declarations indexed from sourceView source ↗

Module documentation

Algebra Formally Smooth exists linear Map eq of symmetric hochschild two cocycle

Imports3
  • Mathlib.RingTheory.Smooth.Basic
  • Mathlib.Tactic.Abel
  • Mathlib.Tactic.Module
Imported by2

Declarations

structure

Cocycle

L36 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Cocycle
Documentation

A symmetric normalized Hochschild two-cocycle with values in the module.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
Lean source · full declaration
structure Cocycle (R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S]
    (M : Type w) [AddCommGroup M] [Module R M] [Module S M] where
  /-- The bilinear two-cocycle. -/
  ψ : S →ₗ[R] S →ₗ[R] M
  /-- The cocycle is symmetric. -/
  symm : ∀ x y, ψ x y = ψ y x
  /-- The cocycle vanishes when the first argument is one. -/
  one : ∀ y, ψ 1 y = 0
  /-- The Hochschild cocycle identity. -/
  coc : ∀ x y z, x • ψ y z - ψ (x * y) z + ψ x (y * z) - z • ψ x y = 0
structure

Ext

L49 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext
Documentation

The underlying pair of a scalar and a module element in the extension defined by the cocycle.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
Lean source · full declaration
structure Ext (c : Cocycle R S M) where
  /-- The scalar component. -/
  fst : S
  /-- The module component. -/
  snd : M
theorem

ext

L59 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.ext
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem ext {a b : Ext c} (h1 : a.fst = b.fst) (h2 : a.snd = b.snd) : a = b
def

equiv

L63 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.equiv
Documentation

The identification of the underlying extension with the Cartesian product.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · full declaration
def equiv : Ext c ≃ S × M where
  toFun a := (a.fst, a.snd)
  invFun q := ⟨q.1, q.2⟩
  left_inv _ := rfl
  right_inv _ := rfl
instance

(anonymous instance)

L69 ↗
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
instance : AddCommGroup (Ext c)
def

addEquiv

L72 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.addEquiv
Documentation

The additive identification of the extension with the product of the two additive groups.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · full declaration
def addEquiv : Ext c ≃+ S × M where
  toEquiv := equiv c
  map_add' _ _ := rfl
instance

instModule

L76 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.instModule
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
instance instModule : Module R (Ext c)
theorem

fst_add

L78 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.fst_add
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem fst_add (a b : Ext c) : (a + b).fst = a.fst + b.fst
theorem

snd_add

L79 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.snd_add
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem snd_add (a b : Ext c) : (a + b).snd = a.snd + b.snd
theorem

fst_zero

L80 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.fst_zero
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem fst_zero : (0 : Ext c).fst = 0
theorem

snd_zero

L81 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.snd_zero
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem snd_zero : (0 : Ext c).snd = 0
theorem

fst_neg

L82 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.fst_neg
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem fst_neg (a : Ext c) : (-a).fst = -a.fst
theorem

snd_neg

L83 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.snd_neg
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem snd_neg (a : Ext c) : (-a).snd = -a.snd
theorem

fst_smul

L84 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.fst_smul
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem fst_smul (r : R) (a : Ext c) : (r • a).fst = r • a.fst
theorem

snd_smul

L85 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.snd_smul
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem snd_smul (r : R) (a : Ext c) : (r • a).snd = r • a.snd
theorem

fst_mk

L86 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.fst_mk
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem fst_mk (x : S) (u : M) : (Ext.mk x u : Ext c).fst = x
theorem

snd_mk

L87 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.snd_mk
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem snd_mk (x : S) (u : M) : (Ext.mk x u : Ext c).snd = u
instance

(anonymous instance)

L89 ↗
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
instance : Mul (Ext c)
instance

(anonymous instance)

L92 ↗
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
instance : One (Ext c)
theorem

fst_mul

L94 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.fst_mul
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem fst_mul (a b : Ext c) : (a * b).fst = a.fst * b.fst
theorem

snd_mul

L95 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.snd_mul
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem snd_mul (a b : Ext c) :
    (a * b).snd = a.fst • b.snd + b.fst • a.snd + c.ψ a.fst b.fst
theorem

fst_one

L97 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.fst_one
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem fst_one : (1 : Ext c).fst = 1
theorem

snd_one

L98 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.snd_one
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem snd_one : (1 : Ext c).snd = 0
theorem

mul_comm'

L100 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.mul_comm'
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem mul_comm' (a b : Ext c) : a * b = b * a
theorem

mul_assoc'

L106 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.mul_assoc'
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem mul_assoc' (a b d : Ext c) : a * b * d = a * (b * d)
theorem

one_mul'

L118 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.one_mul'
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · statement
theorem one_mul' (a : Ext c) : 1 * a = a
instance

instCommRing

L123 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.instCommRing
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
Lean source · full declaration
instance instCommRing : CommRing (Ext c) where
  __ := (inferInstance : AddCommGroup (Ext c))
  mul := (· * ·)
  one := 1
  mul_assoc := mul_assoc' c
  one_mul := one_mul' c
  mul_one a := by rw [mul_comm']; exact one_mul' c a
  zero_mul a := by
    ext
    · simp only [fst_mul, fst_zero, zero_mul]
    · simp only [snd_mul, fst_zero, snd_zero, zero_smul, smul_zero, map_zero,
        LinearMap.zero_apply, add_zero]
  mul_zero a := by
    ext
    · simp only [fst_mul, fst_zero, mul_zero]
    · simp only [snd_mul, fst_zero, snd_zero, zero_smul, smul_zero, map_zero, add_zero]
  left_distrib a b d := by
    ext
    · simp only [fst_mul, fst_add, mul_add]
    · simp only [snd_mul, fst_add, snd_add, smul_add, add_smul, map_add]
      abel
  right_distrib a b d := by
    ext
    · simp only [fst_mul, fst_add, add_mul]
    · simp only [snd_mul, fst_add, snd_add, smul_add, add_smul, map_add, LinearMap.add_apply]
      abel
  mul_comm := mul_comm' c
theorem

smul_mul_assoc'

L153 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.smul_mul_assoc'
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
variable [IsScalarTower R S M]
Lean source · statement
theorem smul_mul_assoc' (r : R) (a b : Ext c) : (r • a) * b = r • (a * b)
instance

instAlgebra

L159 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.instAlgebra
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
variable [IsScalarTower R S M]
Lean source · statement
instance instAlgebra : Algebra R (Ext c)
def

fstHom

L164 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.fstHom
Documentation

The algebra homomorphism projecting the extension to its scalar component.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
variable [IsScalarTower R S M]
Lean source · full declaration
def fstHom : Ext c →ₐ[R] S where
  toFun := Ext.fst
  map_one' := rfl
  map_mul' _ _ := rfl
  map_zero' := rfl
  map_add' _ _ := rfl
  commutes' r := by
    rw [Algebra.algebraMap_eq_smul_one, fst_smul, fst_one, Algebra.algebraMap_eq_smul_one]
theorem

fstHom_apply

L173 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.fstHom_apply
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
variable [IsScalarTower R S M]
Lean source · statement
theorem fstHom_apply (a : Ext c) : fstHom c a = a.fst
theorem

fstHom_surjective

L175 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.fstHom_surjective
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
variable [IsScalarTower R S M]
Lean source · statement
theorem fstHom_surjective : Function.Surjective (fstHom c)
theorem

fst_eq_zero_of_mem_ker

L177 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.fst_eq_zero_of_mem_ker
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
variable [IsScalarTower R S M]
Lean source · statement
theorem fst_eq_zero_of_mem_ker {a : Ext c} (ha : a ∈ RingHom.ker (fstHom c : Ext c →+* S)) :
    a.fst = 0
theorem

ker_sq_eq_bot

L180 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.ker_sq_eq_bot
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
variable [IsScalarTower R S M]
Lean source · statement
theorem ker_sq_eq_bot : RingHom.ker (fstHom c : Ext c →+* S) ^ 2 = ⊥
theorem

isNilpotent_ker

L190 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.isNilpotent_ker
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
variable [IsScalarTower R S M]
Lean source · statement
theorem isNilpotent_ker : IsNilpotent (RingHom.ker (fstHom c : Ext c →+* S))
def

sect

L196 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.sect
Documentation

A section of the extension projection supplied by formal smoothness.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
variable [IsScalarTower R S M]
variable [Algebra.FormallySmooth R S]
Lean source · statement
def sect : S →ₐ[R] Ext c
theorem

fst_sect

L200 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.fst_sect
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
variable [IsScalarTower R S M]
variable [Algebra.FormallySmooth R S]
Lean source · statement
theorem fst_sect (x : S) : (sect c x).fst = x
def

ell

L206 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.ell
Documentation

The linear map given by the module component of the chosen section.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
variable [IsScalarTower R S M]
variable [Algebra.FormallySmooth R S]
Lean source · full declaration
def ell : S →ₗ[R] M where
  toFun x := (sect c x).snd
  map_add' x y := by rw [map_add, snd_add]
  map_smul' r x := by rw [map_smul, snd_smul, RingHom.id_apply]
theorem

ell_apply

L211 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.ell_apply
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
variable [IsScalarTower R S M]
variable [Algebra.FormallySmooth R S]
Lean source · statement
theorem ell_apply (x : S) : ell c x = (sect c x).snd
theorem

ell_one

L213 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.ell_one
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
variable [IsScalarTower R S M]
variable [Algebra.FormallySmooth R S]
Lean source · statement
theorem ell_one : ell c 1 = 0
theorem

ψ_eq

L215 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle.HochschildSplitSol.Ext.ψ_eq
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
noncomputable section
namespace HochschildSplitSol
variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
  {M : Type w} [AddCommGroup M] [Module R M] [Module S M]
namespace Ext
variable (c : Cocycle R S M)
variable [IsScalarTower R S M]
variable [Algebra.FormallySmooth R S]
Lean source · statement
theorem ψ_eq (x y : S) : c.ψ x y = ell c (x * y) - x • ell c y - y • ell c x
theorem

exists_linearMap_eq_of_symmetric_hochschild_two_cocycle

L228 ↗
Algebra.FormallySmooth.exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
universe u v w
open HochschildSplitSol in
Lean source · statement
theorem _root_.Algebra.FormallySmooth.exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
    (R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S] [Algebra.FormallySmooth R S]
    (M : Type w) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    (ψ : S →ₗ[R] S →ₗ[R] M)
    (hsymm : ∀ x y, ψ x y = ψ y x)
    (hone : ∀ y, ψ 1 y = 0)
    (hcoc : ∀ x y z, x • ψ y z - ψ (x * y) z + ψ x (y * z) - z • ψ x y = 0) :
    ∃ l : S →ₗ[R] M, l 1 = 0 ∧ ∀ x y, ψ x y = l (x * y) - x • l y - y • l x

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.