NYLL
Module

TrivialBaseChangeAlgebra.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.TrivialBaseChangeAlgebra
3 declarations indexed from sourceView source ↗

Module documentation

Actual tensor splitting from the pullback action

The tensor spectrum is identified with the literal finite-etale pullback. The fiber comparison then turns triviality of the induced fundamental-group action into a splitting of the actual tensor algebra.

Imports4
Imported by5

Declarations

theorem

pullback_fiber_fixed_of_image_fixed

L33 ↗
AlgebraicGeometry.FiniteEtale.pullback_fiber_fixed_of_image_fixed
Documentation

Triviality of the image action is exactly what is needed on the actual pullback fiber. The canonical pullback-fiber comparison supplies the transport.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem pullback_fiber_fixed_of_image_fixed
    {X Y : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (f : X ⟶ Y) (point : Spec (.of Ω) ⟶ X) (W : FiniteEtale Y)
    (hfixed : ∀ (g : Aut (fiber point)) (w : (fiber (point ≫ f)).obj W),
      fundamentalGroupHom f point g • w = w) :
    ∀ (g : Aut (fiber point)) (w : (fiber point).obj ((pullback f).obj W)),
      g • w = w
theorem

image_fixed_of_pullback_fiber_fixed

L53 ↗
AlgebraicGeometry.FiniteEtale.image_fixed_of_pullback_fiber_fixed
Documentation

Fixedness on the actual pullback fiber gives fixedness under the induced fundamental-group image, using the same canonical fiber comparison.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem image_fixed_of_pullback_fiber_fixed
    {X Y : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (f : X ⟶ Y) (point : Spec (.of Ω) ⟶ X) (W : FiniteEtale Y)
    (hfixed : ∀ (g : Aut (fiber point))
      (w : (fiber point).obj ((pullback f).obj W)), g • w = w) :
    ∀ (g : Aut (fiber point)) (w : (fiber (point ≫ f)).obj W),
      fundamentalGroupHom f point g • w = w
theorem

exists_tensor_algEquiv_pi_of_image_fixed

L70 ↗
AlgebraicGeometry.FiniteEtale.exists_tensor_algEquiv_pi_of_image_fixed
Documentation

A trivial induced action on an affine finite-etale cover supplies an actual algebra isomorphism splitting its scalar extension.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem exists_tensor_algEquiv_pi_of_image_fixed
    (K L B : Type u) [CommRing K] [Field L] [CommRing B]
    [Algebra K L] [Algebra K B]
    [IsFiniteEtale (Spec.map (CommRingCat.ofHom (algebraMap K B)))]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (point : Spec (.of Ω) ⟶ Spec (.of L))
    (hfixed : ∀ (g : Aut (fiber point))
      (w : (fiber (point ≫ Spec.map (CommRingCat.ofHom (algebraMap K L)))).obj
        (mk (Spec.map (CommRingCat.ofHom (algebraMap K B))))),
      fundamentalGroupHom (Spec.map (CommRingCat.ofHom (algebraMap K L))) point g • w = w) :
    ∃ (ι : Type u) (_ : Finite ι), Nonempty ((L ⊗[K] B) ≃ₐ[L] (ι → L))

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