Point derivations

2 fully proved

Algebra

DefinitionPoint derivations of an algebra#✓fully proved

Point derivations at a k-point ev of a k-algebra A with values in a k-module M.

def PointDerivations (k : Type u) (A : Type v) [Field k] [CommRing A] [Algebra k A]
    (ev : A →ₐ[k] k) (M : Type w) [AddCommGroup M] [Module k M] : Submodule k (A →ₗ[k] M) where
  carrier := {D | ∀ a b : A, D (a * b) = ev a • D b + ev b • D a}
  add_mem' := by
    intro D D' hD hD' a b
    simp only [LinearMap.add_apply, hD a b, hD' a b, smul_add]
    ac_rfl
  zero_mem' := by
    intro a b
    simp
  smul_mem' := by
    intro c D hD a b
    simp only [LinearMap.smul_apply, hD a b, smul_add, smul_comm c]

Used by 1

Used byFunctoriality of point derivations in the coefficient module

Point Derivations

DefinitionFunctoriality of point derivations in the coefficient module#✓fully proved

Functoriality of point derivations in the coefficient module.

def map (ev : A →ₐ[k] k) (φ : M →ₗ[k] M') :
    ↥(PointDerivations k A ev M) →ₗ[k] ↥(PointDerivations k A ev M') where
  toFun D := ⟨φ.comp D.1, fun a b => by
    simp only [LinearMap.comp_apply, D.2 a b, map_add, map_smul]⟩
  map_add' D D' := by ext a; simp
  map_smul' c D := by ext a; simp

def PointDerivations (k : Type u) (A : Type v) [Field k] [CommRing A] [Algebra k A]
    (ev : A →ₐ[k] k) (M : Type w) [AddCommGroup M] [Module k M] : Submodule k (A →ₗ[k] M) where
  carrier := {D | ∀ a b : A, D (a * b) = ev a • D b + ev b • D a}
  add_mem' := by
    intro D D' hD hD' a b
    simp only [LinearMap.add_apply, hD a b, hD' a b, smul_add]
    ac_rfl
  zero_mem' := by
    intro a b
    simp
  smul_mem' := by
    intro c D hD a b
  ⋯

MathlibExt/Algebra/PointDerivations.lean:48

Uses 1

Statement usesPoint derivations of an algebra

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.