Documentation

TauCeti.LinearAlgebra.SymmetricAlgebra.Functoriality

Functoriality of symmetric algebras #

A linear map induces an algebra homomorphism between symmetric algebras. This file constructs the map from the universal property, proves its identity and composition laws, and packages linear equivalences as algebra equivalences.

The construction and its lemma set follow Mathlib's CliffordAlgebra.map and ExteriorAlgebra.map functoriality APIs (Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean and Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean).

The declaration order, API naming, and proof organization also adapt the prior Tau Ceti formalization in TauCeti/Algebra/Lie/UniversalEnveloping/Functoriality.lean.

Main definitions #

Main results #

Roadmap #

This supplies the symmetric-algebra side of functoriality for subalgebras and direct sums in Layer 3 of the LieHighestWeight roadmap. The product comparison and naturality of the canonical map to the PBW associated graded are downstream.

source
noncomputable def SymmetricAlgebra.map (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) :
SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R N

The algebra homomorphism between symmetric algebras induced by a linear map.

Equations
Instances For
    source
    @[simp]
    theorem SymmetricAlgebra.map_apply_ι (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (a : M) :
    (map R f) ((ι R M) a) = (ι R N) (f a)

    A symmetric-algebra map acts on canonical generators by the original linear map.

    source
    theorem SymmetricAlgebra.map_unique (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (g : SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R N) :
    (∀ (a : M), g ((ι R M) a) = (ι R N) (f a)) ↔ g = map R f

    The universal property characterizes the induced map by its values on generators.

    source
    @[simp]
    theorem SymmetricAlgebra.map_id (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] :
    map R LinearMap.id = AlgHom.id R (SymmetricAlgebra R M)

    The identity linear map induces the identity algebra homomorphism.

    source
    @[simp]
    theorem SymmetricAlgebra.map_comp_ι (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) :
    (map R f).toLinearMap ∘ₗ ι R M = ι R N ∘ₗ f

    The induced map commutes with the canonical generator maps.

    source
    @[simp]
    theorem SymmetricAlgebra.map_comp_map (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} {P : Type x} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) :
    (map R g).comp (map R f) = map R (g ∘ₗ f)

    Composition of linear maps becomes composition of the induced algebra homomorphisms.

    source
    theorem SymmetricAlgebra.map_leftInverse (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} {g : N →ₗ[R] M} (h : Function.LeftInverse ⇑g ⇑f) :
    Function.LeftInverse ⇑(map R g) ⇑(map R f)

    A left inverse of linear maps induces a left inverse of the corresponding symmetric-algebra maps.

    source
    theorem SymmetricAlgebra.map_rightInverse (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} {g : N →ₗ[R] M} (h : Function.RightInverse ⇑g ⇑f) :
    Function.RightInverse ⇑(map R g) ⇑(map R f)

    A right inverse of linear maps induces a right inverse of the corresponding symmetric-algebra maps.

    source
    theorem SymmetricAlgebra.map_injective_of_leftInverse (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (g : N →ₗ[R] M) (h : Function.LeftInverse ⇑g ⇑f) :
    Function.Injective ⇑(map R f)

    A split monomorphism induces an injective map of symmetric algebras.

    source
    theorem SymmetricAlgebra.map_surjective_of_rightInverse (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (g : N →ₗ[R] M) (h : Function.RightInverse ⇑g ⇑f) :
    Function.Surjective ⇑(map R f)

    A split epimorphism induces a surjective map of symmetric algebras.

    source
    theorem SymmetricAlgebra.map_surjective (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (h : Function.Surjective ⇑f) :
    Function.Surjective ⇑(map R f)

    A surjective linear map induces a surjective map of symmetric algebras.

    source
    noncomputable def SymmetricAlgebra.mapEquiv (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) :
    SymmetricAlgebra R M ≃ₐ[R] SymmetricAlgebra R N

    A linear equivalence induces an algebra equivalence of symmetric algebras.

    Equations
    Instances For
      source
      @[simp]
      theorem SymmetricAlgebra.mapEquiv_toAlgHom (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) :
      ↑(mapEquiv R e) = map R ↑e

      The algebra homomorphism underlying mapEquiv is induced by the underlying linear map.

      source
      @[simp]
      theorem SymmetricAlgebra.mapEquiv_apply (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (a : SymmetricAlgebra R M) :
      (mapEquiv R e) a = (map R ↑e) a

      The induced equivalence agrees with the induced algebra map on every element.

      source
      theorem SymmetricAlgebra.mapEquiv_ι (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (a : M) :
      (mapEquiv R e) ((ι R M) a) = (ι R N) (e a)

      The bundled equivalence acts on canonical generators by the underlying linear equivalence.

      source
      @[simp]
      theorem SymmetricAlgebra.mapEquiv_symm (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) :
      (mapEquiv R e).symm = mapEquiv R e.symm

      Passing the inverse linear equivalence to symmetric algebras gives the inverse algebra equivalence.

      source
      @[simp]
      theorem SymmetricAlgebra.mapEquiv_refl (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] :
      mapEquiv R (LinearEquiv.refl R M) = AlgEquiv.refl

      The identity linear equivalence induces the identity algebra equivalence.

      source
      @[simp]
      theorem SymmetricAlgebra.mapEquiv_trans (R : Type u) [CommSemiring R] {M : Type v} {N : Type w} {P : Type x} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (e : M ≃ₗ[R] N) (d : N ≃ₗ[R] P) :
      (mapEquiv R e).trans (mapEquiv R d) = mapEquiv R (e ≪≫ₗ d)

      Composition of linear equivalences becomes composition of the induced algebra equivalences.