NYLL
Module

CanonicalAlgebraEqualizer.lean

Nyll.SchemeTheory.Descent.CanonicalAlgebraEqualizer
6 declarations indexed from sourceView source ↗

Module documentation

Recovering an algebra from the canonical faithfully flat equalizer

The algebra equalizer is constructed from the actual Amitsur module equalizer. A map into a scalar extension descends when its values are fixed by the canonical coaction. If its scalar extension is bijective, faithful flatness reflects bijectivity of the descended map.

Imports5
Imported by2

Declarations

def

canonicalInvariants

L36 ↗
Algebra.Descent.canonicalInvariants
Documentation

The actual subalgebra fixed by the canonical scalar-extension coaction.

Source context 6 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (S E A : Type u) [CommRing S] [CommRing E] [CommRing A]
variable [Algebra S E] [Algebra S A]
Lean source · statement
def canonicalInvariants : Subalgebra S (E ⊗[S] A)
def

canonicalInvariantsInclusion

L41 ↗
Algebra.Descent.canonicalInvariantsInclusion
Documentation

The coefficient inclusion lands in the canonical equalizer.

Source context 6 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (S E A : Type u) [CommRing S] [CommRing E] [CommRing A]
variable [Algebra S E] [Algebra S A]
Lean source · statement
def canonicalInvariantsInclusion : A →ₐ[S] canonicalInvariants S E A
def

canonicalInvariantsEquiv

L50 ↗
Algebra.Descent.canonicalInvariantsEquiv
Documentation

Faithfully flat descent recovers the original algebra as the canonical coaction's literal equalizer subalgebra.

Source context 6 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (S E A : Type u) [CommRing S] [CommRing E] [CommRing A]
variable [Algebra S E] [Algebra S A]
Lean source · statement
def canonicalInvariantsEquiv [Module.FaithfullyFlat S E] :
    A ≃ₐ[S] canonicalInvariants S E A
def

descendCanonicalAlgHom

L107 ↗
Algebra.Descent.descendCanonicalAlgHom
Documentation

Descend a concrete algebra map whose values satisfy the canonical coaction relation, using the faithfully flat equalizer.

Source context 7 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (S E A : Type u) [CommRing S] [CommRing E] [CommRing A]
variable [Algebra S E] [Algebra S A]
variable (D : Type u) [CommRing D] [Algebra S D]
Lean source · statement
def descendCanonicalAlgHom [Module.FaithfullyFlat S E]
    (φ : D →ₐ[S] E ⊗[S] A)
    (hφ : ∀ d : D, canonicalCoaction S E A (φ d) = (1 : E) ⊗ₜ[S] φ d) :
    D →ₐ[S] A
theorem

descendCanonicalAlgHom_spec

L115 ↗
Algebra.Descent.descendCanonicalAlgHom_spec
Documentation

The descended map has exactly the prescribed coefficient inclusion.

Source context 7 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (S E A : Type u) [CommRing S] [CommRing E] [CommRing A]
variable [Algebra S E] [Algebra S A]
variable (D : Type u) [CommRing D] [Algebra S D]
Lean source · statement
theorem descendCanonicalAlgHom_spec [Module.FaithfullyFlat S E]
    (φ : D →ₐ[S] E ⊗[S] A)
    (hφ : ∀ d : D, canonicalCoaction S E A (φ d) = (1 : E) ⊗ₜ[S] φ d)
    (d : D) :
    (1 : E) ⊗ₜ[S] descendCanonicalAlgHom S E A D φ hφ d = φ d
def

descendCanonicalEquiv

L126 ↗
Algebra.Descent.descendCanonicalEquiv
Documentation

Bijectivity after faithfully flat scalar extension proves that the actual equalizer-descended algebra map is an equivalence.

Source context 7 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (S E A : Type u) [CommRing S] [CommRing E] [CommRing A]
variable [Algebra S E] [Algebra S A]
variable (D : Type u) [CommRing D] [Algebra S D]
Lean source · full declaration
def descendCanonicalEquiv [Module.FaithfullyFlat S E]
    (φ : D →ₐ[S] E ⊗[S] A)
    (hφ : ∀ d : D, canonicalCoaction S E A (φ d) = (1 : E) ⊗ₜ[S] φ d)
    (hbij : Function.Bijective
      (Algebra.TensorProduct.lift (Algebra.ofId E (E ⊗[S] A)) φ
        (fun _ _ ↦ Commute.all _ _))) :
    D ≃ₐ[S] A := by
  let f : D →ₐ[S] A := descendCanonicalAlgHom S E A D φ hφ
  apply AlgEquiv.ofBijective f
  apply (Module.FaithfullyFlat.lTensor_bijective_iff_bijective S E f.toLinearMap).mp
  have hmap : (f.toLinearMap.lTensor E : E ⊗[S] D → E ⊗[S] A) =
      Algebra.TensorProduct.lift (Algebra.ofId E (E ⊗[S] A)) φ
        (fun _ _ ↦ Commute.all _ _) := by
    funext x
    induction x using TensorProduct.inductionOn with
    | tmul e d =>
      rw [LinearMap.lTensor_tmul, Algebra.TensorProduct.lift_tmul,
        ← descendCanonicalAlgHom_spec S E A D φ hφ d]
      change e ⊗ₜ[S] f d =
        (e ⊗ₜ[S] (1 : A)) * ((1 : E) ⊗ₜ[S] f d)
      rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
    | add x y hx hy => simp only [map_add, hx, hy]
  rw [hmap]
  exact hbij

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.