Documentation

TauCeti.Algebra.AlgebraicGroup.Tangent.Cotangent

The cotangent space at the identity #

For a commutative bialgebra A over R, the cotangent space at the identity is the augmentation ideal modulo its square. Its R-linear dual represents counit-valued derivations, hence the tangent space at the identity.

When this cotangent space is finite projective, the usual tensor--Hom comparison identifies B ⊗[R] Lie(G)(R) with the B-valued tangent space. On pure tensors the comparison sends b ⊗ d to the derivation a ↦ b * algebraMap R B (d a). This is the scalar-extension comparison needed to turn the coefficient-natural adjoint action into an action on one fixed finite module (ReductiveGroups roadmap, Layer 2).

Main declarations #

References #

source
@[reducible, inline]
abbrev TauCeti.Bialgebra.AugmentationIdeal (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Bialgebra R A] :
Ideal A

The augmentation ideal of a commutative bialgebra, the kernel of its counit.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev TauCeti.Bialgebra.CotangentSpace (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Bialgebra R A] :
    Type u_2

    The cotangent space at the identity of the affine monoid represented by A: the augmentation ideal ker ε modulo its square.

    Equations
    Instances For
      source
      noncomputable def TauCeti.Bialgebra.cotangentMap (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Bialgebra R A] :
      A →ₗ[R] CotangentSpace R A

      The first-order displacement from the identity, sending a to the class of a - ε(a) in the augmentation ideal modulo its square.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.Bialgebra.cotangentMap_apply (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Bialgebra R A] (a : A) :
        (cotangentMap R A) a = (AugmentationIdeal R A).toCotangent ⟨a - (algebraMap R A) (CoalgebraStruct.counit a), ⋯⟩

        The cotangent map is the class of the displacement from the counit.

        source
        theorem TauCeti.Bialgebra.cotangentMap_one (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Bialgebra R A] :
        (cotangentMap R A) 1 = 0

        The cotangent map vanishes at the identity.

        source
        theorem TauCeti.Bialgebra.cotangentMap_augmentation (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Bialgebra R A] (x : ↥(AugmentationIdeal R A)) :
        (cotangentMap R A) ↑x = (AugmentationIdeal R A).toCotangent x

        On the augmentation ideal, the cotangent map is the quotient map.

        source
        theorem TauCeti.Bialgebra.cotangentMap_mul (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Bialgebra R A] (a b : A) :
        (cotangentMap R A) (a * b) = CoalgebraStruct.counit a • (cotangentMap R A) b + CoalgebraStruct.counit b • (cotangentMap R A) a

        The cotangent displacement of a product satisfies the Leibniz rule for the action through the counit.

        source
        noncomputable def Derivation.cotangentLinearEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing B] [Algebra R B] :
        (TauCeti.Bialgebra.CotangentSpace R A →ₗ[R] B) ≃ₗ[B] Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)

        Linear functionals on the cotangent space are naturally equivalent to counit-valued derivations, i.e. tangent vectors at the identity. The equivalence is linear over the coefficient ring.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem Derivation.cotangentLinearEquiv_apply_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing B] [Algebra R B] (f : TauCeti.Bialgebra.CotangentSpace R A →ₗ[R] B) (a : A) :
          (cotangentLinearEquiv f) a = f ((TauCeti.Bialgebra.cotangentMap R A) a)

          The cotangent-duality equivalence sends a functional to its value on the first-order displacement.

          source
          @[simp]
          theorem Derivation.cotangentLinearEquiv_symm_toCotangent {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing B] [Algebra R B] (d : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)) (x : ↥(TauCeti.Bialgebra.AugmentationIdeal R A)) :
          (cotangentLinearEquiv.symm d) ((TauCeti.Bialgebra.AugmentationIdeal R A).toCotangent x) = (TauCeti.Bialgebra.CounitAlgebra.algEquivSelf R A B) (d ↑x)

          The inverse cotangent-duality equivalence evaluates a derivation on a representative in the augmentation ideal.

          source
          noncomputable def Derivation.tangentScalarExtensionEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing B] [Algebra R B] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R A)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R A)] :
          TensorProduct R B (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R A)) ≃ₗ[B] Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)

          Scalar extension of tangent vectors. If the cotangent space is finite projective, B tensored with its dual is naturally the space of B-valued tangent vectors. The dual is identified with Lie(G)(R) by cotangentLinearEquiv.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Derivation.tangentScalarExtensionEquiv_tmul_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing B] [Algebra R B] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R A)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R A)] (b : B) (f : Module.Dual R (TauCeti.Bialgebra.CotangentSpace R A)) (a : A) :
            (tangentScalarExtensionEquiv (b ⊗ₜ[R] f)) a = b * (algebraMap R B) (f ((TauCeti.Bialgebra.cotangentMap R A) a))

            On pure tensors, scalar extension evaluates the cotangent functional and multiplies it by the coefficient. The bundled pure-tensor simp rule is tangentScalarExtensionEquiv_tmul.

            source
            @[simp]
            theorem Derivation.tangentScalarExtensionEquiv_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing B] [Algebra R B] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R A)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R A)] (b : B) (f : Module.Dual R (TauCeti.Bialgebra.CotangentSpace R A)) :
            tangentScalarExtensionEquiv (b ⊗ₜ[R] f) = b • (mapValue (Algebra.ofId R B)) (cotangentLinearEquiv f)

            On pure tensors, scalar extension is coefficient change of the cotangent-dual tangent vector, followed by multiplication by the tensor coefficient.