Algebraic Group

Results named in Tau Ceti's TauCeti.Algebra.AlgebraicGroup modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremBorel fixed-point theorem, orbit form#

Every nonempty closed invariant subset of projective space contains a rational line whose full scheme-point orbit is a singleton.

TauCeti.Comodule.exists_projectiveOrbitMap_eq_identity_of_isClosed_of_isSolvable.{u}
  {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H]
  [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [Group.IsSolvable (WithConv (H →ₐ[k] k))]
  [AddCommGroup M] [_root_.Module k M] [TauCeti.Comodule k H M] [Module.Finite k M]
  {Z :
    Set
      ↥(AlgebraicGeometry.Proj (TauCeti.SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M)))}
  (hZ : IsClosed Z) (hne : Z.Nonempty)
  (hinvariant :
    ∀ (g : WithConv (H →ₐ[k] k)),
      Set.MapsTo (⇑(TauCeti.Comodule.projectivePointTranslation g).hom) Z Z) :
  ∃ m,
    ∃ (hm : Module.IsUnimodular k m),
      (TauCeti.Comodule.projectiveOrbitMap m hm) (Bialgebra.counitAlgHom k H).kernelPoint ∈ Z ∧
        ∀ (x : ↥(AlgebraicGeometry.Spec ↧H)),
          (TauCeti.Comodule.projectiveOrbitMap m hm) x =
            (TauCeti.Comodule.projectiveOrbitMap m hm) (Bialgebra.counitAlgHom k H).kernelPoint

Lean

Formalized in Tau Ceti as TauCeti.Comodule.exists_projectiveOrbitMap_eq_identity_of_isClosed_of_isSolvable.

Other forms

Borel fixed-point theorem, projective form. Formalized in Tau Ceti as TauCeti.Comodule.exists_fixed_mem_of_isClosed_of_isSolvable.

TauCeti.Comodule.exists_fixed_mem_of_isClosed_of_isSolvable.{u} {k H M : Type u} [Field k]
  [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H]
  [ConnectedSpace (PrimeSpectrum H)] [Group.IsSolvable (WithConv (H →ₐ[k] k))] [AddCommGroup M]
  [_root_.Module k M] [TauCeti.Comodule k H M] [Module.Finite k M]
  {Z :
    Set
      ↥(AlgebraicGeometry.Proj (TauCeti.SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M)))}
  (hZ : IsClosed Z) (hne : Z.Nonempty)
  (hinvariant :
    ∀ (g : WithConv (H →ₐ[k] k)),
      Set.MapsTo (⇑(TauCeti.Comodule.projectivePointTranslation g).hom) Z Z) :
  ∃ x ∈ Z,
    x ∈
        closedPoints
          ↥(AlgebraicGeometry.Proj
              (TauCeti.SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M))) ∧
      ∀ (g : WithConv (H →ₐ[k] k)), (TauCeti.Comodule.projectivePointTranslation g).hom x = x

Sources

• Tau Ceti documentation: TauCeti.Comodule.exists_projectiveOrbitMap_eq_identity_of_isClosed_of_isSolvable
• Source of TauCeti.Comodule.exists_projectiveOrbitMap_eq_identity_of_isClosed_of_isSolvable in TauCeti/Algebra/AlgebraicGroup/Representation/ProjectiveOrbit/FixedPoint/Existence.lean

LeanTauCeti.Comodule.exists_projectiveOrbitMap_eq_identity_of_isClosed_of_isSolvable · TauCeti.Comodule.exists_fixed_mem_of_isClosed_of_isSolvable

Uses 2 · Used by 1

Proof usesThe Jacobian criterion for étaleness · The Lie--Kolchin theorem

Used byBorel conjugacy

TheoremCartier's theorem#

a finite-type commutative Hopf algebra over a field of characteristic zero is smooth. Equivalently, every affine group scheme of finite type over such a field is smooth.

TauCeti.smoothCommHopfAlgProperty_of_charZero.{u, v} (k : Type u) [Field k] [CharZero k]
  (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] : TauCeti.smoothCommHopfAlgProperty k H

Lean

Formalized in Tau Ceti as TauCeti.smoothCommHopfAlgProperty_of_charZero.

Sources

• Tau Ceti documentation: TauCeti.smoothCommHopfAlgProperty_of_charZero
• Source of TauCeti.smoothCommHopfAlgProperty_of_charZero in TauCeti/Algebra/AlgebraicGroup/Smooth/CharZero.lean

LeanTauCeti.smoothCommHopfAlgProperty_of_charZero

Uses 1 · Used by 4

Proof usesThe Jacobian criterion for étaleness

Used byMatsushima's criterion, affine direction, in characteristic zero · Weyl's theorem for algebraic groups · The dimension of a centralizer and of [𝔤, x] · TauCeti.AlgebraicGeometry.smooth_of_grpObj_of_charZero

TheoremChevalley's coset criterion#

A closed subgroup with finitely generated defining ideal admits a finite exterior-power representation and a unimodular vector whose matrix coefficients detect its left cosets over every commutative value algebra, including nonreduced algebras.

TauCeti.HopfIdeal.exists_finite_subcomodule_exteriorPower_coset_matrixCoefficient.{u, v, x}
  {k : Type u} [Field k] {H : CommHopfAlgCat k} (I : TauCeti.HopfIdeal k ↑H) (hI : I.toIdeal.FG) :
  ∃ V n,
    Module.Finite k ↥V.toSubmodule ∧
      let this := Module.addCommMonoidToAddCommGroup k;
      ∃ m,
        Module.IsUnimodular k m ∧
          ∀ (A : CommAlgCat k) (g h : ↑(TauCeti.HopfAlgebra.points A)),
            ↑g = ↑h ↔
              ∃ c,
                ∀ (φ : Module.Dual k ↥(⋀[k]^n ↥V)),
                  h.ofConv (TauCeti.Comodule.matrixCoefficient φ m) =
                    ↑c * g.ofConv (TauCeti.Comodule.matrixCoefficient φ m)

Lean

Formalized in Tau Ceti as TauCeti.HopfIdeal.exists_finite_subcomodule_exteriorPower_coset_matrixCoefficient.

Sources

• Tau Ceti documentation: TauCeti.HopfIdeal.exists_finite_subcomodule_exteriorPower_coset_matrixCoefficient
• Source of TauCeti.HopfIdeal.exists_finite_subcomodule_exteriorPower_coset_matrixCoefficient in TauCeti/Algebra/AlgebraicGroup/Representation/ProjectiveOrbit/LineFibers.lean

LeanTauCeti.HopfIdeal.exists_finite_subcomodule_exteriorPower_coset_matrixCoefficient

Uses 1

Proof usesChevalley's theorem with the subgroup character

TheoremChevalley's theorem with the subgroup character#

A closed subgroup with finitely generated defining ideal is the stabilizer, over every commutative value algebra, of a line in a finite-dimensional exterior-power representation. The line lies in the weight space of a unique character of the subgroup, including when the subgroup is nonreduced.

TauCeti.HopfIdeal.exists_finite_subcomodule_exteriorPower_line_stabilizer.{u, v, w} {k : Type u}
  [Field k] {H : CommHopfAlgCat k} (I : TauCeti.HopfIdeal k ↑H) (hI : I.toIdeal.FG) :
  ∃ V n,
    Module.Finite k ↥V.toSubmodule ∧
      let this := Module.addCommMonoidToAddCommGroup k;
      ∃ L,
        Module.finrank k ↥L = 1 ∧
          (∃! χ, L ≤ I.weightSpace (↥(⋀[k]^n ↥V)) χ) ∧
            ∀ (A : CommAlgCat k) (g : ↑(TauCeti.HopfAlgebra.points A)),
              g ∈ TauCeti.CommHopfAlgCat.quotientPointsSubgroup H I A ↔
                Submodule.map (TauCeti.Comodule.endOfPoint (↥(⋀[k]^n ↥V)) g.ofConv)
                    (Submodule.baseChange (↑A) L) =
                  Submodule.baseChange (↑A) L

Lean

Formalized in Tau Ceti as TauCeti.HopfIdeal.exists_finite_subcomodule_exteriorPower_line_stabilizer.

Sources

• Tau Ceti documentation: TauCeti.HopfIdeal.exists_finite_subcomodule_exteriorPower_line_stabilizer
• Source of TauCeti.HopfIdeal.exists_finite_subcomodule_exteriorPower_line_stabilizer in TauCeti/Algebra/AlgebraicGroup/Representation/ExteriorStabilizer/Character.lean

LeanTauCeti.HopfIdeal.exists_finite_subcomodule_exteriorPower_line_stabilizer

Used by 1

Used byChevalley's coset criterion

TheoremDeligne's theorem (TauCeti.AlgHom.convPow_eq_one_of_rankAtStalk)#

Every point of a commutative and cocommutative Hopf algebra which is finite flat of constant stalk rank n over R is killed by n.

TauCeti.AlgHom.convPow_eq_one_of_rankAtStalk.{u_1, u_2, u_3} {R : Type u_1} {H : Type u_2}
  [CommRing R] [CommRing H] [HopfAlgebra R H] [Coalgebra.IsCocomm R H] [Module.Finite R H]
  [Module.Flat R H] {n : ℕ} (hn : ∀ (p : PrimeSpectrum R), Module.rankAtStalk H p = n)
  {A : Type u_3} [CommSemiring A] [Algebra R A] (x : WithConv (H →ₐ[R] A)) : x ^ n = 1

Lean

Formalized in Tau Ceti as TauCeti.AlgHom.convPow_eq_one_of_rankAtStalk.

Other forms

Deligne's theorem, free case. Formalized in Tau Ceti as TauCeti.AlgHom.convPow_finrank_eq_one.

TauCeti.AlgHom.convPow_finrank_eq_one.{u_1, u_2, u_3} {R : Type u_1} {H : Type u_2} [CommRing R]
  [CommRing H] [HopfAlgebra R H] [Coalgebra.IsCocomm R H] [Module.Free R H] [Module.Finite R H]
  {A : Type u_3} [CommSemiring A] [Algebra R A] (x : WithConv (H →ₐ[R] A)) :
  x ^ Module.finrank R H = 1

Sources

• Tau Ceti documentation: TauCeti.AlgHom.convPow_eq_one_of_rankAtStalk
• Source of TauCeti.AlgHom.convPow_eq_one_of_rankAtStalk in TauCeti/Algebra/AlgebraicGroup/KilledByRank.lean

LeanTauCeti.AlgHom.convPow_eq_one_of_rankAtStalk · TauCeti.AlgHom.convPow_finrank_eq_one

Used by 1

Used byDeligne's theorem (TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.pow_eq_one_of_finrank)

TheoremThe dynamic Levi decomposition, on points#

every point of the dynamic parabolic is a point of its unipotent part times a point of its Levi part.

TauCeti.Cocharacter.exists_mem_unipotent_mem_levi.{u_1, u_2, u_3} {R : Type u_1} {H : Type u_2}
  {A : Type u_3} [CommSemiring R] [Semiring H] [CommSemiring A] [Algebra R A] [HopfAlgebra R H]
  {l : H →ₐc[R] LaurentPolynomial R} {g : WithConv (H →ₐ[R] A)}
  (hg : g ∈ TauCeti.Cocharacter.parabolic A l) :
  ∃ u ∈ TauCeti.Cocharacter.unipotent A l, ∃ z ∈ TauCeti.Cocharacter.levi A l, g = u * z

Lean

Formalized in Tau Ceti as TauCeti.Cocharacter.exists_mem_unipotent_mem_levi.

Sources

• Tau Ceti documentation: TauCeti.Cocharacter.exists_mem_unipotent_mem_levi
• Source of TauCeti.Cocharacter.exists_mem_unipotent_mem_levi in TauCeti/Algebra/AlgebraicGroup/Dynamic/Parabolic.lean

LeanTauCeti.Cocharacter.exists_mem_unipotent_mem_levi

DefinitionThe fppf first isomorphism theorem for affine groups#

If f : H ⟶ K is faithfully flat and of finite presentation, then the fppf quotient of Spec K by the kernel of the represented homomorphism Spec K ⟶ Spec H is represented by Spec H.

TauCeti.CommHopfAlgCat.kernelFppfQuotientIso.{u} {R : Type u} [CommRing R] {H K : CommHopfAlgCat R}
  (f : H ⟶ K) (hflat : (↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat)
  (hfp : (↑(CommHopfAlgCat.Hom.hom f)).FinitePresentation) :
  TauCeti.CommHopfAlgCat.fppfQuotientSheaf K (TauCeti.CommHopfAlgCat.kernelHopfIdeal f) ⋯ ≅
    TauCeti.CommHopfAlgCat.pointsFppfGroupObject H

Lean

Formalized in Tau Ceti as TauCeti.CommHopfAlgCat.kernelFppfQuotientIso.

Sources

• Tau Ceti documentation: TauCeti.CommHopfAlgCat.kernelFppfQuotientIso
• Source of TauCeti.CommHopfAlgCat.kernelFppfQuotientIso in TauCeti/Algebra/AlgebraicGroup/Fppf/Quotient/Kernel.lean

LeanTauCeti.CommHopfAlgCat.kernelFppfQuotientIso

TheoremKolchin's theorem for 𝔾ₐ#

every nonzero vector of a comodule over the coordinate algebra of the additive group produces a nonzero fixed vector, over an arbitrary base and with no finiteness hypothesis. The witness is the top nonvanishing divided-power component Nᵢ v: by the binomial composition rule each further component of it is a component of v of strictly larger index, which vanishes by maximality.

TauCeti.AdditiveGroup.exists_ne_zero_coact_eq_tmul_one.{u, v} (R : Type u) [CommSemiring R]
  {V : Type v} [AddCommMonoid V] [_root_.Module R V] [TauCeti.Comodule R (SymmetricAlgebra R R) V]
  {v : V} (hv : v ≠ 0) : ∃ w, w ≠ 0 ∧ TauCeti.Comodule.coact w = w ⊗ₜ[R] 1

Lean

Formalized in Tau Ceti as TauCeti.AdditiveGroup.exists_ne_zero_coact_eq_tmul_one.

Sources

• Tau Ceti documentation: TauCeti.AdditiveGroup.exists_ne_zero_coact_eq_tmul_one
• Source of TauCeti.AdditiveGroup.exists_ne_zero_coact_eq_tmul_one in TauCeti/Algebra/AlgebraicGroup/AdditiveGroup/Unipotent.lean

LeanTauCeti.AdditiveGroup.exists_ne_zero_coact_eq_tmul_one

TheoremThe Lie--Kolchin theorem#

If the rational points of a reduced connected affine group of finite type over an algebraically closed field form a solvable group, every finite-dimensional representation admits a basis in which its coefficient matrix is upper triangular, with characters on the diagonal.

TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_isSolvable.{u, v, w}
  {k : Type u} {H : Type v} {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H]
  [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [_root_.Module k M]
  [TauCeti.Comodule k H M] [FiniteDimensional k M] [ConnectedSpace (PrimeSpectrum H)]
  [Group.IsSolvable (WithConv (H →ₐ[k] k))] :
  ∃ n b,
    (TauCeti.Comodule.coefficientMatrix b).IsUpperTriangular ∧
      ∀ (i : Fin n), IsGroupLikeElem k (TauCeti.Comodule.coefficientMatrix b i i)

Lean

Formalized in Tau Ceti as TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_isSolvable.

Other forms

Lie--Kolchin for GLₙ-valued points. Formalized in Tau Ceti as TauCeti.GeneralLinear.exists_map_inv_mul_mul_map_mem_upperTriangularGroup.

TauCeti.GeneralLinear.exists_map_inv_mul_mul_map_mem_upperTriangularGroup.{u, v} {k : Type u}
  [Field k] {n : ℕ} [IsAlgClosed k] {Q : Type v} [CommRing Q] [HopfAlgebra k Q]
  [Algebra.FiniteType k Q] [IsReduced Q]
  (hconn : TauCeti.geometricallyConnectedCommHopfAlgProperty k ↧Q)
  (hsolv : TauCeti.geometricallySolvablePointsCommHopfAlgProperty k ↧Q)
  (π : ↑(TauCeti.GeneralLinear.coordinateHopfAlgebra k n) →ₐc[k] Q) :
  ∃ P,
    (Matrix.GeneralLinearGroup.map (algebraMap k Q)) P⁻¹ *
          (TauCeti.GeneralLinear.pointsMulEquiv n) (WithConv.toConv ↑π) *
        (Matrix.GeneralLinearGroup.map (algebraMap k Q)) P ∈
      TauCeti.upperTriangularGroup (Fin n) Q

Lie--Kolchin for Sp₂ₘ-valued points. Formalized in Tau Ceti as TauCeti.Symplectic.IsotropicFlag.exists_map_inv_mul_mul_map_mem_matrixSubgroup.

TauCeti.Symplectic.IsotropicFlag.exists_map_inv_mul_mul_map_mem_matrixSubgroup.{u, v} {k : Type u}
  [Field k] {m : ℕ} {Q : Type v} [CommRing Q] [HopfAlgebra k Q] [IsAlgClosed k]
  [Algebra.FiniteType k Q] [IsReduced Q]
  (hconn : TauCeti.geometricallyConnectedCommHopfAlgProperty k ↧Q)
  (hsolv : TauCeti.geometricallySolvablePointsCommHopfAlgProperty k ↧Q)
  (π : ↑(TauCeti.Symplectic.coordinateHopfAlgebra k m) →ₐc[k] Q) :
  ∃ P,
    (TauCeti.GLSymplecticFin.map m k (algebraMap k Q)) P⁻¹ *
          (TauCeti.Symplectic.pointsMulEquiv k m) (WithConv.toConv ↑π) *
        (TauCeti.GLSymplecticFin.map m k (algebraMap k Q)) P ∈
      TauCeti.GLSymplecticFin.IsotropicFlag.matrixSubgroup m

The Lie--Kolchin theorem for the geometric object properties. Formalized in Tau Ceti as TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_geometricallySolvable.

TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_geometricallySolvable.{u, v, w}
  {k : Type u} {H : Type v} {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H]
  [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [_root_.Module k M]
  [TauCeti.Comodule k H M] [FiniteDimensional k M]
  (hconn : TauCeti.geometricallyConnectedCommHopfAlgProperty k ↧H)
  (hsolv : TauCeti.geometricallySolvablePointsCommHopfAlgProperty k ↧H) :
  ∃ n b,
    (TauCeti.Comodule.coefficientMatrix b).IsUpperTriangular ∧
      ∀ (i : Fin n), IsGroupLikeElem k (TauCeti.Comodule.coefficientMatrix b i i)

Lie--Kolchin under unipotence of the derived subgroup. Formalized in Tau Ceti as TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_forall_isUnipotentPoint_derived.

TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_forall_isUnipotentPoint_derived.{u,
    v, w}
  {k : Type u} {H : Type v} {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H]
  [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [_root_.Module k M]
  [TauCeti.Comodule k H M] [FiniteDimensional k M]
  (hderived :
    ∀ (g : WithConv (↑((↧H).quotient (TauCeti.CommHopfAlgCat.derivedDefiningIdeal H)) →ₐ[k] k)),
      TauCeti.HopfAlgebra.IsUnipotentPoint g) :
  ∃ n b,
    (TauCeti.Comodule.coefficientMatrix b).IsUpperTriangular ∧
      ∀ (i : Fin n), IsGroupLikeElem k (TauCeti.Comodule.coefficientMatrix b i i)

Lie--Kolchin, geometric weight-vector form. Formalized in Tau Ceti as TauCeti.Comodule.hasNonzeroWeightVector_of_geometricallySolvable.

TauCeti.Comodule.hasNonzeroWeightVector_of_geometricallySolvable.{u, v, w} {k : Type u} {H : Type v}
  {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H]
  [IsReduced H] [AddCommGroup M] [_root_.Module k M] [TauCeti.Comodule k H M]
  [FiniteDimensional k M] [Nontrivial M]
  (hconn : TauCeti.geometricallyConnectedCommHopfAlgProperty k ↧H)
  (hsolv : TauCeti.geometricallySolvablePointsCommHopfAlgProperty k ↧H) :
  TauCeti.Comodule.HasNonzeroWeightVector k H M

Lie--Kolchin, weight-vector form. Formalized in Tau Ceti as TauCeti.Comodule.hasNonzeroWeightVector_of_isSolvable.

TauCeti.Comodule.hasNonzeroWeightVector_of_isSolvable.{u, v, w} {k : Type u} {H : Type v}
  {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H]
  [IsReduced H] [AddCommGroup M] [_root_.Module k M] [TauCeti.Comodule k H M]
  [FiniteDimensional k M] [Nontrivial M] [ConnectedSpace (PrimeSpectrum H)]
  [Group.IsSolvable (WithConv (H →ₐ[k] k))] : TauCeti.Comodule.HasNonzeroWeightVector k H M

Sources

• Tau Ceti documentation: TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_isSolvable
• Source of TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_isSolvable in TauCeti/Algebra/AlgebraicGroup/Solvable/LieKolchin.lean

LeanTauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_isSolvable · TauCeti.GeneralLinear.exists_map_inv_mul_mul_map_mem_upperTriangularGroup · TauCeti.Symplectic.IsotropicFlag.exists_map_inv_mul_mul_map_mem_matrixSubgroup · TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_geometricallySolvable · TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_forall_isUnipotentPoint_derived · TauCeti.Comodule.hasNonzeroWeightVector_of_geometricallySolvable · TauCeti.Comodule.hasNonzeroWeightVector_of_isSolvable

Uses 1 · Used by 2

Proof usesKolchin's common fixed vector theorem

Used byBorel fixed-point theorem, orbit form · Matsushima's criterion, affine direction, in characteristic zero

TheoremMatsushima's criterion, affine direction, in characteristic zero#

For a reductive closed subgroup N of an affine group G of finite type over a field of characteristic zero, restriction to the invariant functions identifies the fppf homogeneous quotient G/N with the sheaf of points of Spec O(G)^N.

TauCeti.HopfIdeal.isIso_fppfHomogeneousQuotientToCoinvariantsPoints_of_reductive.{u} {k : Type u}
  [Field k] [CharZero k] {H : TauCeti.FiniteTypeCommHopfAlgCat k} (I : TauCeti.HopfIdeal k ↑H.obj)
  (hred : TauCeti.reductiveCommHopfAlgProperty k (H.quotient I)) :
  CategoryTheory.IsIso I.fppfHomogeneousQuotientToCoinvariantsPoints

Lean

Formalized in Tau Ceti as TauCeti.HopfIdeal.isIso_fppfHomogeneousQuotientToCoinvariantsPoints_of_reductive.

Other forms

Matsushima's criterion for a closed immersion, in characteristic zero. Formalized in Tau Ceti as TauCeti.HopfIdeal.isIso_fppfHomogeneousQuotientToCoinvariantsPoints_ker_of_reductive.

TauCeti.HopfIdeal.isIso_fppfHomogeneousQuotientToCoinvariantsPoints_ker_of_reductive.{u}
  {k : Type u} [Field k] [CharZero k] {H K : TauCeti.FiniteTypeCommHopfAlgCat k} (f : H ⟶ K)
  (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f.hom))
  (hK : TauCeti.reductiveCommHopfAlgProperty k K) :
  CategoryTheory.IsIso
    (TauCeti.HopfIdeal.ker
        (CommHopfAlgCat.Hom.hom f.hom)).fppfHomogeneousQuotientToCoinvariantsPoints

Sources

• Tau Ceti documentation: TauCeti.HopfIdeal.isIso_fppfHomogeneousQuotientToCoinvariantsPoints_of_reductive
• Source of TauCeti.HopfIdeal.isIso_fppfHomogeneousQuotientToCoinvariantsPoints_of_reductive in TauCeti/Algebra/AlgebraicGroup/Fppf/Quotient/Homogeneous/Coinvariants.lean

LeanTauCeti.HopfIdeal.isIso_fppfHomogeneousQuotientToCoinvariantsPoints_of_reductive · TauCeti.HopfIdeal.isIso_fppfHomogeneousQuotientToCoinvariantsPoints_ker_of_reductive

Uses 6 · Used by 1

Proof usesCartier's theorem · Hilbert's finiteness theorem · Kolchin's common fixed vector theorem · The Lie--Kolchin theorem · Weyl's complete reducibility theorem · Weyl's theorem as a decomposition

Used byGLₙ/G is affine for a faithful reductive representation

DefinitionPointwise first isomorphism theorem for affine groups#

If the morphism represented by f is surjective on A-points, the target group of points is isomorphic to the pointwise quotient of source points by the scheme-theoretic kernel.

TauCeti.CommHopfAlgCat.kernelPointwiseQuotientIso.{u, v, w} {R : Type u} [CommRing R]
  {H K : CommHopfAlgCat R} (f : H ⟶ K) (A : CommAlgCat R)
  (hsurj :
    Function.Surjective
      ⇑(CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.Hom.mapPointsFunctor f).app A))) :
  TauCeti.CommHopfAlgCat.pointwiseQuotientGroup K (TauCeti.CommHopfAlgCat.kernelHopfIdeal f) ⋯ A ≅
    TauCeti.HopfAlgebra.points A

Lean

Formalized in Tau Ceti as TauCeti.CommHopfAlgCat.kernelPointwiseQuotientIso.

Sources

• Tau Ceti documentation: TauCeti.CommHopfAlgCat.kernelPointwiseQuotientIso
• Source of TauCeti.CommHopfAlgCat.kernelPointwiseQuotientIso in TauCeti/Algebra/AlgebraicGroup/HopfIdeal/Quotient/Kernel/Presheaf.lean

LeanTauCeti.CommHopfAlgCat.kernelPointwiseQuotientIso

TheoremWeyl's theorem for algebraic groups#

Over an algebraically closed field of characteristic zero, every finite-dimensional representation of a connected group whose Lie algebra has nondegenerate Killing form is completely reducible.

TauCeti.Comodule.isCompletelyReducible_of_isKilling.{u, w} {k : Type u} [Field k] [CharZero k]
  [IsAlgClosed k] {H : TauCeti.FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)]
  [LieAlgebra.IsKilling k (Derivation k (↑H.obj) (TauCeti.Bialgebra.CounitAlgebra k (↑H.obj) k))]
  {M : Type w} [AddCommGroup M] [_root_.Module k M] [TauCeti.Comodule k (↑H.obj) M]
  [FiniteDimensional k M] : TauCeti.Comodule.IsCompletelyReducible k (↑H.obj) M

Lean

Formalized in Tau Ceti as TauCeti.Comodule.isCompletelyReducible_of_isKilling.

Sources

• Tau Ceti documentation: TauCeti.Comodule.isCompletelyReducible_of_isKilling
• Source of TauCeti.Comodule.isCompletelyReducible_of_isKilling in TauCeti/Algebra/AlgebraicGroup/Representation/CompleteReducibility.lean

LeanTauCeti.Comodule.isCompletelyReducible_of_isKilling

Uses 2

Proof usesCartier's theorem · Weyl's complete reducibility theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.