Multiplicative bases

MultiplicativeBasisDeformations.Foundations.CornerAlgebra

Corner algebras #

For an idempotent e of a k-algebra A, Mathlib's corner ring IsIdempotentElem.Corner is eAe with identity e. This file makes it a k-algebra, with c ↦ c • e as structure map.

source
def MultiplicativeBasisDeformations.cornerVal {A : Type v} [Ring A] {e : A} (idem : IsIdempotentElem e) (x : idem.Corner) :
A

The underlying element of A of an element of the corner.

Instances For
    source
    def MultiplicativeBasisDeformations.cornerMk {A : Type v} [Ring A] {e : A} (idem : IsIdempotentElem e) (a : A) (ha : a ∈ Subsemigroup.corner e) :
    idem.Corner

    An element of A lying in the corner, as an element of the corner.

    Instances For
      source
      theorem MultiplicativeBasisDeformations.cornerVal_mem {A : Type v} [Ring A] {e : A} (idem : IsIdempotentElem e) (x : idem.Corner) :
      cornerVal idem x ∈ Subsemigroup.corner e
      source
      theorem MultiplicativeBasisDeformations.corner_ext {A : Type v} [Ring A] {e : A} (idem : IsIdempotentElem e) {x y : idem.Corner} (h : cornerVal idem x = cornerVal idem y) :
      x = y
      source
      theorem MultiplicativeBasisDeformations.corner_ext_iff {A : Type v} [Ring A] {e : A} {idem : IsIdempotentElem e} {x y : idem.Corner} :
      x = y ↔ cornerVal idem x = cornerVal idem y
      source
      @[simp]
      theorem MultiplicativeBasisDeformations.cornerVal_mk {A : Type v} [Ring A] {e : A} (idem : IsIdempotentElem e) (a : A) (ha : a ∈ Subsemigroup.corner e) :
      cornerVal idem (cornerMk idem a ha) = a
      source
      theorem MultiplicativeBasisDeformations.corner_smul_mem {k : Type u} [CommRing k] {A : Type v} [Ring A] [Algebra k A] {e : A} (idem : IsIdempotentElem e) (c : k) (x : idem.Corner) :
      c • cornerVal idem x ∈ Subsemigroup.corner e
      source
      @[instance_reducible]
      instance MultiplicativeBasisDeformations.cornerSMul {k : Type u} [CommRing k] {A : Type v} [Ring A] [Algebra k A] {e : A} (idem : IsIdempotentElem e) :
      SMul k idem.Corner
      source
      @[simp]
      theorem MultiplicativeBasisDeformations.corner_smul_val {k : Type u} [CommRing k] {A : Type v} [Ring A] [Algebra k A] {e : A} (idem : IsIdempotentElem e) (c : k) (x : idem.Corner) :
      cornerVal idem (c • x) = c • cornerVal idem x
      source
      @[simp]
      theorem MultiplicativeBasisDeformations.corner_one_val {A : Type v} [Ring A] {e : A} (idem : IsIdempotentElem e) :
      cornerVal idem 1 = e
      source
      @[simp]
      theorem MultiplicativeBasisDeformations.corner_mul_val {A : Type v} [Ring A] {e : A} (idem : IsIdempotentElem e) (x y : idem.Corner) :
      cornerVal idem (x * y) = cornerVal idem x * cornerVal idem y
      source
      @[simp]
      theorem MultiplicativeBasisDeformations.corner_add_val {A : Type v} [Ring A] {e : A} (idem : IsIdempotentElem e) (x y : idem.Corner) :
      cornerVal idem (x + y) = cornerVal idem x + cornerVal idem y
      source
      @[simp]
      theorem MultiplicativeBasisDeformations.corner_zero_val {A : Type v} [Ring A] {e : A} (idem : IsIdempotentElem e) :
      cornerVal idem 0 = 0
      source
      theorem MultiplicativeBasisDeformations.corner_mul_left {A : Type v} [Ring A] {e : A} (idem : IsIdempotentElem e) (x : idem.Corner) :
      e * cornerVal idem x = cornerVal idem x
      source
      theorem MultiplicativeBasisDeformations.corner_mul_right {A : Type v} [Ring A] {e : A} (idem : IsIdempotentElem e) (x : idem.Corner) :
      cornerVal idem x * e = cornerVal idem x
      source
      @[instance_reducible]
      instance MultiplicativeBasisDeformations.cornerAlgebra {k : Type u} [CommRing k] {A : Type v} [Ring A] [Algebra k A] {e : A} (idem : IsIdempotentElem e) :
      Algebra k idem.Corner

      The corner eAe is a k-algebra.