Nyll.SchemeTheory.FiniteEtale.Algebra.FaithfullyFlatDescent

Module documentation

Finite étale invariant algebras

The equalizer algebra constructed by faithfully flat descent is itself finite étale when the algebra carrying the coaction is finite étale. The comparison with its scalar extension is the actual invariant-subalgebra map, so the native descent theorems for finiteness and étaleness apply to this construction.

theorem

invariants_finite_etale

L38 ↗

Algebra.FaithfullyFlatDescent.invariants_finite_etale

Documentation

The actual invariant algebra of a finite étale algebra coaction is finite étale over the original ring.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.FaithfullyFlatDescent
variable {R B : Type u} [CommRing R] [CommRing B]

Lean source · full declaration

theorem invariants_finite_etale (f : R →+* B) (C : Type u)
    [CommRing C] [Algebra B C] [Module.Finite B C] [Algebra.Etale B C]
    (hf : f.FaithfullyFlat)
    (ρ :
      letI : Algebra R B := f.toAlgebra
      letI : Algebra R C := Algebra.compHom C f
      C →ₐ[B] B ⊗[R] C)
    (hε : coactionLinear f C ρ ≫
        (ModuleCat.extendRestrictScalarsAdj f).toComonad.ε.app (ModuleCat.of B C) =
      𝟙 (ModuleCat.of B C))
    (hδ : coactionLinear f C ρ ≫
        (ModuleCat.extendRestrictScalarsAdj f).toComonad.δ.app (ModuleCat.of B C) =
      coactionLinear f C ρ ≫
        (ModuleCat.extendRestrictScalarsAdj f).toComonad.map (coactionLinear f C ρ)) :
    Module.Finite R (invariants f C ρ) ∧ Algebra.Etale R (invariants f C ρ) := by
  let : Algebra R B := f.toAlgebra
  let : Algebra R C := Algebra.compHom C f
  let : Module.FaithfullyFlat R B := hf
  let e : B ⊗[R] invariants f C ρ ≃ₐ[B] C :=
    invariantsBaseChangeEquiv f C hf ρ hε hδ
  let : Module.Finite B (B ⊗[R] invariants f C ρ) :=
    Module.Finite.equiv e.symm.toLinearEquiv
  let : Algebra.Etale B (B ⊗[R] invariants f C ρ) := Algebra.Etale.of_equiv e.symm
  exact ⟨Module.Finite.of_finite_tensorProduct_of_faithfullyFlat B,
    Algebra.Etale.of_etale_tensorProduct_of_faithfullyFlat B⟩

Module documentation

Finite étale invariant algebras

Declarations

invariants_finite_etale