Faithfully flat descent for the functor of points

Let A → B be a faithfully flat extension of commutative R-algebras. The two maps B ⇉ B ⊗[A] B give two restriction maps on the B-points represented by a Hopf algebra H. This file proves that the A-points are exactly the B-points on which those restrictions agree, as an equivalence of groups. The coordinate algebra need not be commutative for this algebraic descent statement; the affine-group-scheme application specializes to commutative H.

The proof uses Mathlib's effective-descent theorem Algebra.IsEffective.of_faithfullyFlat: the equalizer of B ⇉ B ⊗[A] B is the image of A. Rather than repeating its elementwise argument for points, we package that equalizer as an algebra equivalence and precompose algebra maps out of H. The resulting equivalence respects convolution because it is induced by postcomposition in the value algebra.

This is the affine, group-valued faithfully flat descent statement needed by the fppf sheaf and quotient lane of the reductive-groups roadmap. The finite-presentation part of an fppf cover is not needed for descent itself, so the result is stated at the natural faithfully flat level.

Main declarations

• TauCeti.AlgHom.descentSubgroup: the subgroup of B-points satisfying the equalizer condition over B ⊗[A] B.
• TauCeti.AlgHom.faithfullyFlatDescentMulEquiv: A-points are equivalent to that descent subgroup.

References

This is the affine representable case of faithfully flat descent. The algebraic input is Mathlib's Algebra.IsEffective.of_faithfullyFlat, following the standard Amitsur equalizer A → B ⇉ B ⊗[A] B.

noncomputable def TauCeti.AlgHom.descentSubgroup {R : Type u} {H : Type v} (A : Type w) (B : Type x) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] : Subgroup (WithConv (H →ₐ[R] B))

The subgroup of B-points satisfying the descent equalizer condition along A → B.

A point f : H →ₐ[R] B belongs to this subgroup exactly when its two postcompositions H →ₐ[R] B ⇉ B ⊗[A] B agree. The subgroup structure comes from functoriality of convolution in the value algebra.

Equations

• TauCeti.AlgHom.descentSubgroup A B = (TauCeti.AlgHom.mapValue (TauCeti.AlgHom.faithfullyFlatDescentLeft✝ A B)).eqLocus (TauCeti.AlgHom.mapValue (TauCeti.AlgHom.faithfullyFlatDescentRight✝ A B))

@[simp]

theorem TauCeti.AlgHom.mem_descentSubgroup_iff_apply {R : Type u} {H : Type v} (A : Type w) (B : Type x) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (f : WithConv (H →ₐ[R] B)) : f ∈ descentSubgroup A B ↔ ∀ (h : H), Algebra.TensorProduct.includeLeft (f.ofConv h) = Algebra.TensorProduct.includeRight (f.ofConv h)

Pointwise form of the descent equalizer condition.

noncomputable def TauCeti.AlgHom.faithfullyFlatDescentMulEquiv {R : Type u} {H : Type v} (A : Type w) (B : Type x) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Module.FaithfullyFlat A B] : WithConv (H →ₐ[R] A) ≃* ↥(descentSubgroup A B)

Faithfully flat descent for affine group-valued points. If B is faithfully flat over A, base change identifies the convolution group of A-points of H with the subgroup of B-points whose two restrictions to B ⊗[A] B agree.

Equations

• TauCeti.AlgHom.faithfullyFlatDescentMulEquiv A B = MulEquiv.ofBijective (TauCeti.AlgHom.faithfullyFlatDescentHom✝ A B) ⋯

@[simp]

theorem TauCeti.AlgHom.faithfullyFlatDescentMulEquiv_apply {R : Type u} {H : Type v} (A : Type w) (B : Type x) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Module.FaithfullyFlat A B] (f : WithConv (H →ₐ[R] A)) : ↑((faithfullyFlatDescentMulEquiv A B) f) = (mapValue (IsScalarTower.toAlgHom R A B)) f

The faithfully flat descent equivalence sends an A-point to its base change to B.

@[simp]

theorem TauCeti.AlgHom.mapValue_faithfullyFlatDescentMulEquiv_symm_apply {R : Type u} {H : Type v} (A : Type w) (B : Type x) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Module.FaithfullyFlat A B] (f : ↥(descentSubgroup A B)) : WithConv.toConv ((IsScalarTower.toAlgHom R A B).comp ((faithfullyFlatDescentMulEquiv A B).symm f).ofConv) = ↑f

Descending a compatible B-point and extending it back to B recovers the original point.