Constant finite commutative group schemes

For a finite commutative group G, the constant group scheme over R has coordinate algebra the finite product R^G. Its Hopf structure is pullback along the structure maps of G:

• Δ(f)(a,b) = f(a*b),
• ε(f) = f(1), and
• S(f)(a) = f(a⁻¹).

We use a universe-preserving ULift of the function ring. Besides preventing an accidental collision with Mathlib's unrelated direct-product coalgebra instance, this keeps the coordinate algebra in the universe required by AffineCommGroupScheme.

@[reducible, inline]

abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates (R G : Type u) : Type u

Coordinates of the constant scheme on G: a universe-preserving copy of R^G.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates R G = ULift.{0, ?u.1} (G → R)

def AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.uncurryAlgEquiv {R : Type u} [CommRing R] {G : Type u} : (G → G → R) ≃ₐ[R] G × G → R

Uncurry a two-variable function, with the order adapted to piScalarRight.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.tensorEval {R : Type u} [CommRing R] {G : Type u} [Fintype G] : TensorProduct R (ConstantCoordinates R G) (ConstantCoordinates R G) ≃ₐ[R] G × G → R

Evaluate a tensor of functions on a pair. On pure tensors this is tensorEval (x ⊗ y) (a,b) = x(a) * y(b).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.tensorEval_tmul {R : Type u} [CommRing R] {G : Type u} [Fintype G] (x y : ConstantCoordinates R G) (a b : G) : tensorEval (x ⊗ₜ[R] y) (a, b) = x.down a * y.down b

def AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.mulPullbackAlgHom {R : Type u} [CommRing R] {G : Type u} [CommGroup G] : ConstantCoordinates R G →ₐ[R] G × G → R

Pull functions back along multiplication in G.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.comulAlgHom {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] : ConstantCoordinates R G →ₐ[R] TensorProduct R (ConstantCoordinates R G) (ConstantCoordinates R G)

The comultiplication of the coordinate Hopf algebra of a constant group.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.tensorEval_comulAlgHom {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] (f : ConstantCoordinates R G) (a b : G) : tensorEval (comulAlgHom f) (a, b) = f.down (a * b)

def AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.counitAlgHom {R : Type u} [CommRing R] {G : Type u} [CommGroup G] : ConstantCoordinates R G →ₐ[R] R

Pull functions back along the identity element of G.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.counitAlgHom_apply {R : Type u} [CommRing R] {G : Type u} [CommGroup G] (f : ConstantCoordinates R G) : counitAlgHom f = f.down 1

def AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.antipodeAlgHom {R : Type u} [CommRing R] {G : Type u} [CommGroup G] : ConstantCoordinates R G →ₐ[R] ConstantCoordinates R G

Pull functions back along inversion in G.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.antipodeAlgHom_down_apply {R : Type u} [CommRing R] {G : Type u} [CommGroup G] (f : ConstantCoordinates R G) (g : G) : (antipodeAlgHom f).down g = f.down g⁻¹

def AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.evaluation {R : Type u} [CommRing R] {G : Type u} (g : G) : ConstantCoordinates R G →ₐ[R] R

Evaluation at a group element, viewed as a point of the affine constant scheme.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.evaluation_apply {R : Type u} [CommRing R] {G : Type u} (g : G) (f : ConstantCoordinates R G) : (evaluation g) f = f.down g

def AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.pullbackAlgHom {R : Type u} [CommRing R] {G : Type u} [CommGroup G] {H : Type u} [CommGroup H] (f : G →* H) : ConstantCoordinates R H →ₐ[R] ConstantCoordinates R G

Pull functions back along a homomorphism of the indexing groups.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.pullbackAlgHom_down_apply {R : Type u} [CommRing R] {G : Type u} [CommGroup G] {H : Type u} [CommGroup H] (f : G →* H) (x : ConstantCoordinates R H) (g : G) : ((pullbackAlgHom f) x).down g = x.down (f g)

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.pullbackAlgHom_injective {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Nontrivial R] {H : Type u} [CommGroup H] {f g : G →* H} (h : pullbackAlgHom f = pullbackAlgHom g) : f = g

Over a nonzero base ring, pullback on the function algebra remembers the indexing map.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.lift_evaluation_evaluation {R : Type u} [CommRing R] {G : Type u} [Fintype G] (t : TensorProduct R (ConstantCoordinates R G) (ConstantCoordinates R G)) (g h : G) : (Algebra.TensorProduct.lift (evaluation g) (evaluation h) ⋯) t = tensorEval t (g, h)

Tensoring two evaluation maps is evaluation on the corresponding ordered pair.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.tensorEval_map_pullback {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] {H : Type u} [CommGroup H] [Fintype H] (f : G →* H) (t : TensorProduct R (ConstantCoordinates R H) (ConstantCoordinates R H)) (g h : G) : tensorEval ((Algebra.TensorProduct.map (pullbackAlgHom f) (pullbackAlgHom f)) t) (g, h) = tensorEval t (f g, f h)

Tensor evaluation is natural under pullback along a group homomorphism.

def AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.uncurryTripleAlgEquiv {R : Type u} [CommRing R] {G : Type u} : (G × G → G → R) ≃ₐ[R] G × G × G → R

Uncurry a function on a pair and one further variable.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.rightTripleEval {R : Type u} [CommRing R] {G : Type u} [Fintype G] : TensorProduct R (ConstantCoordinates R G) (TensorProduct R (ConstantCoordinates R G) (ConstantCoordinates R G)) ≃ₐ[R] G × G × G → R

Evaluate a right-associated triple tensor on three group elements.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.rightTripleEval_tmul {R : Type u} [CommRing R] {G : Type u} [Fintype G] (x : ConstantCoordinates R G) (y : TensorProduct R (ConstantCoordinates R G) (ConstantCoordinates R G)) (a b c : G) : rightTripleEval (x ⊗ₜ[R] y) (a, b, c) = x.down a * tensorEval y (b, c)

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.rightTripleEval_assoc_tmul {R : Type u} [CommRing R] {G : Type u} [Fintype G] (x : TensorProduct R (ConstantCoordinates R G) (ConstantCoordinates R G)) (y : ConstantCoordinates R G) (a b c : G) : rightTripleEval ((Algebra.TensorProduct.assoc R R R (ConstantCoordinates R G) (ConstantCoordinates R G) (ConstantCoordinates R G)) (x ⊗ₜ[R] y)) (a, b, c) = tensorEval x (a, b) * y.down c

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.rightTripleEval_assoc_map_comul_id {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] (t : TensorProduct R (ConstantCoordinates R G) (ConstantCoordinates R G)) (a b c : G) : rightTripleEval (↑(Algebra.TensorProduct.assoc R R R (ConstantCoordinates R G) (ConstantCoordinates R G) (ConstantCoordinates R G)) ((Algebra.TensorProduct.map comulAlgHom (AlgHom.id R (ConstantCoordinates R G))) t)) (a, b, c) = tensorEval t (a * b, c)

Evaluating Δ ⊗ id amounts to multiplying the first two input coordinates.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.rightTripleEval_map_id_comul {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] (t : TensorProduct R (ConstantCoordinates R G) (ConstantCoordinates R G)) (a b c : G) : rightTripleEval ((Algebra.TensorProduct.map (AlgHom.id R (ConstantCoordinates R G)) comulAlgHom) t) (a, b, c) = tensorEval t (a, b * c)

Evaluating id ⊗ Δ amounts to multiplying the last two input coordinates.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.lid_map_counit_id_down_apply {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] (t : TensorProduct R (ConstantCoordinates R G) (ConstantCoordinates R G)) (g : G) : ((Algebra.TensorProduct.lid R (ConstantCoordinates R G)) ((Algebra.TensorProduct.map counitAlgHom (AlgHom.id R (ConstantCoordinates R G))) t)).down g = tensorEval t (1, g)

Applying the left unit isomorphism after ε ⊗ id evaluates a tensor at (1,g).

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.rid_map_id_counit_down_apply {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] (t : TensorProduct R (ConstantCoordinates R G) (ConstantCoordinates R G)) (g : G) : ((Algebra.TensorProduct.rid R R (ConstantCoordinates R G)) ((Algebra.TensorProduct.map (AlgHom.id R (ConstantCoordinates R G)) counitAlgHom) t)).down g = tensorEval t (g, 1)

Applying the right unit isomorphism after id ⊗ ε evaluates a tensor at (g,1).

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.comulAlgHom_coassoc {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] : (↑(Algebra.TensorProduct.assoc R R R (ConstantCoordinates R G) (ConstantCoordinates R G) (ConstantCoordinates R G))).comp ((Algebra.TensorProduct.map comulAlgHom (AlgHom.id R (ConstantCoordinates R G))).comp comulAlgHom) = (Algebra.TensorProduct.map (AlgHom.id R (ConstantCoordinates R G)) comulAlgHom).comp comulAlgHom

Coassociativity of pullback along the group multiplication.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.comulAlgHom_rTensor_counit {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] : (Algebra.TensorProduct.map counitAlgHom (AlgHom.id R (ConstantCoordinates R G))).comp comulAlgHom = ↑(Algebra.TensorProduct.lid R (ConstantCoordinates R G)).symm

Left counitality of pullback along multiplication.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.comulAlgHom_lTensor_counit {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] : (Algebra.TensorProduct.map (AlgHom.id R (ConstantCoordinates R G)) counitAlgHom).comp comulAlgHom = ↑(Algebra.TensorProduct.rid R R (ConstantCoordinates R G)).symm

Right counitality of pullback along multiplication.

@[instance_reducible]

noncomputable instance AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.instBialgebra {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] : Bialgebra R (ConstantCoordinates R G)

The bialgebra structure on functions on a finite group.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.bialgebra_comulAlgHom {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] : Bialgebra.comulAlgHom R (ConstantCoordinates R G) = comulAlgHom

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.bialgebra_counitAlgHom {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] : Bialgebra.counitAlgHom R (ConstantCoordinates R G) = counitAlgHom

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.lift_antipode_id_down_apply {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] (t : TensorProduct R (ConstantCoordinates R G) (ConstantCoordinates R G)) (g : G) : ((Algebra.TensorProduct.lift antipodeAlgHom (AlgHom.id R (ConstantCoordinates R G)) ⋯) t).down g = tensorEval t (g⁻¹, g)

Multiplication after applying inversion in the first tensor coordinate evaluates at (g⁻¹,g).

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.lift_id_antipode_down_apply {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] (t : TensorProduct R (ConstantCoordinates R G) (ConstantCoordinates R G)) (g : G) : ((Algebra.TensorProduct.lift (AlgHom.id R (ConstantCoordinates R G)) antipodeAlgHom ⋯) t).down g = tensorEval t (g, g⁻¹)

Multiplication after applying inversion in the second tensor coordinate evaluates at (g,g⁻¹).

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.antipodeAlgHom_mul_left {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] : (Algebra.TensorProduct.lift antipodeAlgHom (AlgHom.id R (ConstantCoordinates R G)) ⋯).comp (Bialgebra.comulAlgHom R (ConstantCoordinates R G)) = (Algebra.ofId R (ConstantCoordinates R G)).comp (Bialgebra.counitAlgHom R (ConstantCoordinates R G))

The first antipode identity for functions on a group.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.antipodeAlgHom_mul_right {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] : (Algebra.TensorProduct.lift (AlgHom.id R (ConstantCoordinates R G)) antipodeAlgHom ⋯).comp (Bialgebra.comulAlgHom R (ConstantCoordinates R G)) = (Algebra.ofId R (ConstantCoordinates R G)).comp (Bialgebra.counitAlgHom R (ConstantCoordinates R G))

The second antipode identity for functions on a group.

@[instance_reducible]

noncomputable instance AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.instHopfAlgebra {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] : HopfAlgebra R (ConstantCoordinates R G)

The Hopf algebra structure on functions on a finite group.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.instHopfAlgebra = HopfAlgebra.ofAlgHom AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.antipodeAlgHom ⋯ ⋯

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.pullbackBialgHom {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] {H : Type u} [CommGroup H] [Fintype H] (f : G →* H) : ConstantCoordinates R H →ₐc[R] ConstantCoordinates R G

Pullback along a group homomorphism is a morphism of the function Hopf algebras.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.pullbackBialgHom f = BialgHom.ofAlgHom (AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.pullbackAlgHom f) ⋯ ⋯

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.evaluation_convMul {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] (g h : G) : WithConv.toConv (evaluation g) * WithConv.toConv (evaluation h) = WithConv.toConv (evaluation (g * h))

Distinguished affine points of the constant scheme multiply as the underlying group does.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.tensorEval_comm {R : Type u} [CommRing R] {G : Type u} [Fintype G] (t : TensorProduct R (ConstantCoordinates R G) (ConstantCoordinates R G)) (a b : G) : tensorEval ((TensorProduct.comm R (ConstantCoordinates R G) (ConstantCoordinates R G)) t) (a, b) = tensorEval t (b, a)

Swapping tensor factors swaps the two evaluation coordinates.

instance AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.instIsCocomm {R : Type u} [CommRing R] {G : Type u} [CommGroup G] [Fintype G] : Coalgebra.IsCocomm R (ConstantCoordinates R G)

The coordinate Hopf algebra is cocommutative when G is commutative.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.constant (R : Type u) [CommRing R] (G : Type u) [CommGroup G] [Fintype G] : AffineFiniteFreeCommGroupScheme R

The finite-free affine constant group scheme on a finite commutative group G.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.constantMapAffine (R : Type u) [CommRing R] {G H : Type u} [CommGroup G] [Fintype G] [CommGroup H] [Fintype H] (f : G →* H) : constant R G ⟶ constant R H

A group homomorphism induces the corresponding morphism of constant affine group schemes.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantMapAffine_coordinateMap (R : Type u) [CommRing R] {G H : Type u} [CommGroup G] [Fintype G] [CommGroup H] [Fintype H] (f : G →* H) : AffineCommGroupScheme.coordinateMap (constantMapAffine R f).hom = ConstantCoordinates.pullbackBialgHom f

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantMapAffine_comp (R : Type u) [CommRing R] {G H K : Type u} [CommGroup G] [Fintype G] [CommGroup H] [Fintype H] [CommGroup K] [Fintype K] (f : G →* H) (g : H →* K) : constantMapAffine R (g.comp f) = CategoryTheory.CategoryStruct.comp (constantMapAffine R f) (constantMapAffine R g)

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantMapAffine_injective (R : Type u) [CommRing R] [Nontrivial R] {G H : Type u} [CommGroup G] [Fintype G] [CommGroup H] [Fintype H] : Function.Injective (constantMapAffine R)

Over a nonzero base ring, the constant affine group-scheme construction is faithful.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.constantScheme (R : Type u) [CommRing R] (G : Type u) [CommGroup G] [Fintype G] : FiniteFlatCommGroupScheme (Spec (CommRingCat.of R))

The geometric realization of the constant finite group scheme.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.constantScheme R G = (AlgebraicGeometry.FiniteFlatCommGroupScheme.constant R G).realize

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.constantMap (R : Type u) [CommRing R] {G H : Type u} [CommGroup G] [Fintype G] [CommGroup H] [Fintype H] (f : G →* H) : constantScheme R G ⟶ constantScheme R H

The geometric morphism of constant finite-flat group schemes induced by a group homomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantMap_comp (R : Type u) [CommRing R] {G H K : Type u} [CommGroup G] [Fintype G] [CommGroup H] [Fintype H] [CommGroup K] [Fintype K] (f : G →* H) (g : H →* K) : constantMap R (g.comp f) = CategoryTheory.CategoryStruct.comp (constantMap R f) (constantMap R g)

The geometric constant-group construction respects composition. This is a concrete downstream consumer of the finite-free realization functor's composition law.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.constantSchemeIsoOfMulEquiv (R : Type u) [CommRing R] {G H : Type u} [CommGroup G] [Fintype G] [CommGroup H] [Fintype H] (e : G ≃* H) : constantScheme R G ≅ constantScheme R H

An isomorphism of finite commutative groups induces an isomorphism of their constant finite-flat group schemes.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.constantBaseChangeAlgEquiv {R K : Type u} [CommRing R] [CommRing K] [Algebra R K] (G : Type u) [CommGroup G] [Fintype G] : TensorProduct R K (ConstantCoordinates R G) ≃ₐ[K] ConstantCoordinates K G

Scalar extension commutes with the function-ring coordinates of a finite constant group. On a pure tensor, this sends s ⊗ f to the function g ↦ algebraMap R K (f g) * s.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantBaseChangeAlgEquiv_tmul {R K : Type u} [CommRing R] [CommRing K] [Algebra R K] (G : Type u) [CommGroup G] [Fintype G] (s : K) (f : ConstantCoordinates R G) (g : G) : ((constantBaseChangeAlgEquiv G) (s ⊗ₜ[R] f)).down g = (algebraMap R K) (f.down g) * s

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.constantBaseChangeBialgEquiv {R K : Type u} [CommRing R] [CommRing K] [Algebra R K] (G : Type u) [CommGroup G] [Fintype G] : TensorProduct R K (ConstantCoordinates R G) ≃ₐc[K] ConstantCoordinates K G

The scalar-extension equivalence for constant coordinates respects the full bialgebra structure, hence also the Hopf structure.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantBaseChangeBialgEquiv_apply {R K : Type u} [CommRing R] [CommRing K] [Algebra R K] (G : Type u) [CommGroup G] [Fintype G] (x : TensorProduct R K (ConstantCoordinates R G)) : (constantBaseChangeBialgEquiv G) x = (constantBaseChangeAlgEquiv G) x

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantBaseChangeBialgEquiv_natural {R K : Type u} [CommRing R] [CommRing K] [Algebra R K] {G H : Type u} [CommGroup G] [Fintype G] [CommGroup H] [Fintype H] (f : G →* H) : (constantBaseChangeBialgEquiv G).toBialgHom.comp (Bialgebra.TensorProduct.map (BialgHom.id K K) (ConstantCoordinates.pullbackBialgHom f)) = (ConstantCoordinates.pullbackBialgHom f).comp (constantBaseChangeBialgEquiv H).toBialgHom

The constant-coordinate base-change equivalence is natural in the finite group.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantBaseChangeBialgEquiv_symm_natural {R K : Type u} [CommRing R] [CommRing K] [Algebra R K] {G H : Type u} [CommGroup G] [Fintype G] [CommGroup H] [Fintype H] (f : G →* H) : (Bialgebra.TensorProduct.map (BialgHom.id K K) (ConstantCoordinates.pullbackBialgHom f)).comp (constantBaseChangeBialgEquiv H).symm.toBialgHom = (constantBaseChangeBialgEquiv G).symm.toBialgHom.comp (ConstantCoordinates.pullbackBialgHom f)

Naturality of the inverse constant-coordinate base-change equivalence, in the orientation used by morphisms of affine schemes.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.constantAffineBaseChangeIso {R K : Type u} [CommRing R] [CommRing K] [Algebra R K] (G : Type u) [CommGroup G] [Fintype G] : (constant R G).baseChange ≅ constant K G

Coordinate scalar extension of a constant affine group is canonically the named constant affine group over the new base.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantAffineBaseChangeIso_naturality {R K : Type u} [CommRing R] [CommRing K] [Algebra R K] {G H : Type u} [CommGroup G] [Fintype G] [CommGroup H] [Fintype H] (f : G →* H) : CategoryTheory.CategoryStruct.comp (AffineFiniteFreeCommGroupScheme.baseChangeFunctor.map (constantMapAffine R f)) (constantAffineBaseChangeIso H).hom = CategoryTheory.CategoryStruct.comp (constantAffineBaseChangeIso G).hom (constantMapAffine K f)

The named constant-coordinate base-change isomorphism is natural in the finite group. This is the affine Hopf presentation of the commutative square later used by quotient filtrations.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.constantRealizeBaseChangeIso {R K : Type u} [CommRing R] [CommRing K] [Algebra R K] (G : Type u) [CommGroup G] [Fintype G] : (baseChange (Spec.map (CommRingCat.ofHom (algebraMap R K)))).obj (constantScheme R G) ≅ (constant R G).baseChange.realize

Geometric base change of a constant finite group scheme agrees with scalar extension of its function Hopf algebra.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.constantRealizeBaseChangeIso G = (AlgebraicGeometry.FiniteFlatCommGroupScheme.constant R G).realizeBaseChangeIso

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.constantBaseChangeIso {R K : Type u} [CommRing R] [CommRing K] [Algebra R K] (G : Type u) [CommGroup G] [Fintype G] : (baseChange (Spec.map (CommRingCat.ofHom (algebraMap R K)))).obj (constantScheme R G) ≅ constantScheme K G

Geometric base change of a constant finite group scheme is canonically the named constant scheme over the new base.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantBaseChangeIso_naturality {R K : Type u} [CommRing R] [CommRing K] [Algebra R K] {G H : Type u} [CommGroup G] [Fintype G] [CommGroup H] [Fintype H] (f : G →* H) : CategoryTheory.CategoryStruct.comp ((baseChange (Spec.map (CommRingCat.ofHom (algebraMap R K)))).map (constantMap R f)) (constantBaseChangeIso H).hom = CategoryTheory.CategoryStruct.comp (constantBaseChangeIso G).hom (constantMap K f)

Geometric base change of constant group morphisms commutes with the named constant-family identifications. Unlike a bare equivalence of point sets, this is an equality of finite-flat group-scheme morphisms and can therefore be used as a filtration square.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.constantPoint (R : Type u) [CommRing R] (G : Type u) [CommGroup G] [Fintype G] (g : G) : (constant R G).Point R

The geometric point of the constant group scheme selected by g.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.constantGeometricPoint (R : Type u) [CommRing R] (G : Type u) [CommGroup G] [Fintype G] (g : G) : (constantScheme R G).Point (AffineCommGroupScheme.testObject R)

The same distinguished point with its finite-flat geometric realization type exposed.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.constantGeometricPoint R G g = AlgebraicGeometry.FiniteFlatCommGroupScheme.constantPoint R G g

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.pointToAlgHom_constantPoint (R : Type u) [CommRing R] (G : Type u) [CommGroup G] [Fintype G] (g : G) : (constant R G).obj.pointToAlgHom R (constantPoint R G g) = ConstantCoordinates.evaluation g

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.mapPoint_constantMap_constantPoint (R : Type u) [CommRing R] {G H : Type u} [CommGroup G] [Fintype G] [CommGroup H] [Fintype H] (f : G →* H) (g : G) : (mapPoint (constantMap R f) (AffineCommGroupScheme.testObject R)) (constantGeometricPoint R G g) = constantGeometricPoint R H (f g)

The geometric map of constant schemes acts on distinguished points by the original group homomorphism.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantPoint_mul (R : Type u) [CommRing R] (G : Type u) [CommGroup G] [Fintype G] (g h : G) : constantPoint R G (g * h) = constantPoint R G g * constantPoint R G h

The distinguished geometric points preserve the multiplication of G.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantPoint_injective (R : Type u) [CommRing R] [Nontrivial R] (G : Type u) [CommGroup G] [Fintype G] : Function.Injective (constantPoint R G)

Distinct indices give distinct distinguished points over every nonzero base ring.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantPoint_surjective_of_noZeroDivisors (R : Type u) [CommRing R] [NoZeroDivisors R] [Nontrivial R] (G : Type u) [CommGroup G] [Fintype G] : Function.Surjective (constantPoint R G)

Over an integral domain, every section of a finite constant scheme is one of its distinguished constant sections.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.constantPointMulEquiv_of_noZeroDivisors (R : Type u) [CommRing R] [NoZeroDivisors R] [Nontrivial R] (G : Type u) [CommGroup G] [Fintype G] : G ≃* (constantScheme R G).Point (AffineCommGroupScheme.testObject R)

Over an integral domain, the indexing group is multiplicatively equivalent to all global sections of its constant finite group scheme.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.basis (R : Type u) [CommRing R] (G : Type u) [CommGroup G] [Fintype G] : Module.Basis G R (ConstantCoordinates R G)

The standard basis of the coordinate ring R^G.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantCoordinates.basis R G = (Pi.basisFun R G).map ULift.moduleEquiv.symm

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constant_order (R : Type u) [CommRing R] [Nontrivial R] (G : Type u) [CommGroup G] [Fintype G] : (constant R G).order = Fintype.card G

The finite-free coordinate rank of the constant group scheme is the cardinality of G.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantScheme_orderAt (R : Type u) [CommRing R] [Nontrivial R] (G : Type u) [CommGroup G] [Fintype G] (s : ↥(Spec (CommRingCat.of R))) : (constantScheme R G).orderAt s = Fintype.card G

The geometric order function of a constant group scheme has the expected value.