Module

FieldPoints.lean

Nyll.EtaleFundamentalGroups.Pi1.GeometricFiber.FieldPoints

9 declarations indexed from sourceView source ↗

Module documentation

Field-valued points and automorphism actions

The upstream-derived actions on algebra homomorphisms and field-point morphisms, the comparison with homomorphisms on global sections, and the detection of field automorphisms by finite etale points.

Imports5

Nyll.EtaleFundamentalGroups.Pi1.FiniteEtale.GaloisCategory
Mathlib.FieldTheory.Galois.Profinite
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Nyll.SchemeTheory.Pi1.FiniteEtale.Geometry

Imported by2

instance

(anonymous instance)

L43 ↗

Source context 5 commands

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

@[expose] public section
universe u
open CategoryTheory
section
variable {k K : Type*} [Field k] [Field K] [Algebra k K]

Lean source · full declaration

instance (L : Type*) [Semiring L] [Algebra k L] : MulAction (K ≃ₐ[k] K) (L →ₐ[k] K) where
  smul g x := (g : _ →ₐ[k] _).comp x
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

instance

(anonymous instance)

L48 ↗

Source context 5 commands

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

@[expose] public section
universe u
open CategoryTheory
section
variable {k K : Type*} [Field k] [Field K] [Algebra k K]

Lean source · statement

instance (L : Type*) [Field L] [Algebra k L] [Algebra L K] [IsScalarTower k L K] [Normal k L]
    [Normal k K] :
    MulAction.IsPretransitive (K ≃ₐ[k] K) (L →ₐ[k] K)

instance

(anonymous instance)

L89 ↗

Source context 8 commands

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

@[expose] public section
universe u
open CategoryTheory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ S)
variable (k K Ω : Type u) [Field k] [Field K] [Algebra k K] [Field Ω] [Algebra k Ω]
  [Algebra K Ω] [IsScalarTower k K Ω]
variable (X : FiniteEtale (Spec (.of k)))

Lean source · full declaration

instance : MulAction (K ≃ₐ[k] K) (Over.mk (ξ k K) ⟶ X.toComma) where
  smul g x := by
    let σ : (Over.mk (ξ k K)).left ⟶ (Over.mk (ξ k K)).left := by
      change Spec (.of K) ⟶ Spec (.of K)
      exact Spec.map (CommRingCat.ofHom (g : K →+* K))
    let σOver : Over.mk (ξ k K) ⟶ Over.mk (ξ k K) :=
      Over.homMk σ (by
        change Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫ ξ k K = ξ k K
        rw [← Spec.map_comp, ← CommRingCat.ofHom_comp, ← AlgEquiv.toAlgHom_toRingHom,
          AlgHom.comp_algebraMap])
    exact σOver ≫ x
  one_smul x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((1 : K ≃ₐ[k] K) : K →+* K)) ≫ x.left = x.left
    simp [AlgEquiv.aut_one]
  mul_smul g h x := by
    ext1
    change Spec.map (CommRingCat.ofHom ((g * h : K ≃ₐ[k] K) : K →+* K)) ≫ x.left =
      Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫
        Spec.map (CommRingCat.ofHom (h : K →+* K)) ≫ x.left
    simp [AlgEquiv.aut_mul, Category.assoc]

lemma

algEquiv_smul_hom

L112 ↗

AlgebraicGeometry.FiniteEtale.algEquiv_smul_hom

Source context 8 commands

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

@[expose] public section
universe u
open CategoryTheory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ S)
variable (k K Ω : Type u) [Field k] [Field K] [Algebra k K] [Field Ω] [Algebra k Ω]
  [Algebra K Ω] [IsScalarTower k K Ω]
variable (X : FiniteEtale (Spec (.of k)))

Lean source · statement

lemma algEquiv_smul_hom (g : K ≃ₐ[k] K) (x : Over.mk (ξ k K) ⟶ X.toComma) :
    (g • x).left = Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫ x.left

instance

(anonymous instance)

L116 ↗

Source context 8 commands

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

@[expose] public section
universe u
open CategoryTheory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ S)
variable (k K Ω : Type u) [Field k] [Field K] [Algebra k K] [Field Ω] [Algebra k Ω]
  [Algebra K Ω] [IsScalarTower k K Ω]
variable (X : FiniteEtale (Spec (.of k)))

Lean source · statement

instance : TopologicalSpace (Over.mk (ξ k K) ⟶ X.toComma)

instance

(anonymous instance)

L119 ↗

Source context 8 commands

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

@[expose] public section
universe u
open CategoryTheory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ S)
variable (k K Ω : Type u) [Field k] [Field K] [Algebra k K] [Field Ω] [Algebra k Ω]
  [Algebra K Ω] [IsScalarTower k K Ω]
variable (X : FiniteEtale (Spec (.of k)))

Lean source · statement

instance : MulAction (K ≃ₐ[k] K) ((forget _ ⋙ coyoneda.obj ⟨Over.mk (ξ k K)⟩).obj X)

def

homEquivAlgHom

L126 ↗

AlgebraicGeometry.FiniteEtale.homEquivAlgHom

Documentation

Identify morphisms from the field point to a finite etale scheme with algebra homomorphisms from its global sections to the field.

Source context 8 commands

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

@[expose] public section
universe u
open CategoryTheory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ S)
variable (k K Ω : Type u) [Field k] [Field K] [Algebra k K] [Field Ω] [Algebra k Ω]
  [Algebra K Ω] [IsScalarTower k K Ω]
variable (X : FiniteEtale (Spec (.of k)))

Lean source · full declaration

def homEquivAlgHom (X : FiniteEtale (Spec (.of k))) :
    (Over.mk (ξ k K) ⟶ X.toComma) ≃ (Γ(X.left, ⊤) →ₐ[k] K) where
  toFun x :=
    { __ := RingHom.comp (Scheme.ΓSpecIso _).hom.hom x.left.appTop.hom,
      commutes' a := by
        have hbase :
            algebraMap k Γ(X.left, ⊤) =
              X.hom.appTop.hom.comp (Scheme.ΓSpecIso (.of k)).inv.hom := by
          simp [RingHom.algebraMap_toAlgebra, Iso.commRingCatIsoToRingEquiv,
            RingEquiv.coe_ringHom_ofRingHom, Scheme.Hom.appTop, Scheme.Hom.app_eq_appLE]
        have h :
            (Scheme.ΓSpecIso (.of k)).inv ≫ X.hom.appTop ≫ x.left.appTop ≫
                (Scheme.ΓSpecIso (.of K)).hom =
              CommRingCat.ofHom (algebraMap k K) := by
          have hx := Over.w x
          change x.left ≫ X.hom = ξ k K at hx
          calc
            (Scheme.ΓSpecIso (.of k)).inv ≫ X.hom.appTop ≫ x.left.appTop ≫
                (Scheme.ΓSpecIso (.of K)).hom =
              (Scheme.ΓSpecIso (.of k)).inv ≫
                (x.left ≫ X.hom).appTop ≫ (Scheme.ΓSpecIso (.of K)).hom := by
                  rw [Scheme.Hom.comp_appTop]
                  exact congrArg
                    (fun q ↦ (Scheme.ΓSpecIso (.of k)).inv ≫ q)
                    (Category.assoc X.hom.appTop x.left.appTop
                      (Scheme.ΓSpecIso (.of K)).hom).symm
            _ = (Scheme.ΓSpecIso (.of k)).inv ≫
                (ξ k K).appTop ≫ (Scheme.ΓSpecIso (.of K)).hom := by
                  rw [hx]
            _ = CommRingCat.ofHom (algebraMap k K) := by
                  rw [Scheme.ΓSpecIso_naturality]
                  simp
        rw [hbase]
        change (Scheme.ΓSpecIso (.of K)).hom.hom
          (x.left.appTop.hom
            (X.hom.appTop.hom ((Scheme.ΓSpecIso (.of k)).inv.hom a))) =
          (algebraMap k K) a
        have ha :=
          congrArg (fun f : CommRingCat.of k ⟶ CommRingCat.of K ↦ f.hom a) h
        rw [CommRingCat.comp_apply, CommRingCat.comp_apply, CommRingCat.comp_apply] at ha
        exact ha }
  invFun x := Over.homMk
      (Spec.map (CommRingCat.ofHom x.toRingHom :
        Γ(X.left, ⊤) ⟶ CommRingCat.of K) ≫ X.left.isoSpec.inv) <| by
    have := x.comp_algebraMap
    dsimp
    rw [← this]
    simp only [Category.assoc, CommRingCat.ofHom_comp, Spec.map_comp]
    congr
    rw [RingHom.algebraMap_toAlgebra]
    dsimp only [OverClass.fromOver_over, RingEquiv.toRingHom_eq_coe, CommRingCat.ofHom_comp,
      CommRingCat.ofHom_hom]
    rw [Spec.map_comp, Scheme.Hom.appLE]
    simp only [TopologicalSpace.Opens.map_top]
    rw [← Scheme.isoSpec_inv_naturality, Scheme.isoSpec_Spec_inv]
    have hiso : (Scheme.ΓSpecIso (.of k)).inv =
        CommRingCat.ofHom (Scheme.ΓSpecIso (.of k)).commRingCatIsoToRingEquiv.symm.toRingHom := by
      ext a
      rfl
    rw [hiso]
    simp [Scheme.Hom.appTop, Scheme.Hom.app_eq_appLE]
  left_inv x := by
    ext1
    simp only [Over.homMk_left]
    rw [CommRingCat.ofHom_comp, CommRingCat.ofHom_hom, CommRingCat.ofHom_hom,
      Spec.map_comp, SpecMap_ΓSpecIso_hom]
    let f : Spec (.of K) ⟶ X.left := x.left
    change ((Spec (.of K)).toSpecΓ ≫ Spec.map f.appTop) ≫ X.left.isoSpec.inv = f
    rw [← Scheme.toSpecΓ_naturality f]
    simp
  right_inv x := by
    apply AlgHom.coe_ringHom_injective
    simp only [Over.homMk_left]
    change (Scheme.ΓSpecIso (.of K)).hom.hom.comp
        ((Spec.map (CommRingCat.ofHom x.toRingHom :
          Γ(X.left, ⊤) ⟶ CommRingCat.of K) ≫ X.left.isoSpec.inv).appTop.hom) =
      x.toRingHom
    rw [← CommRingCat.hom_comp, Scheme.Hom.comp_appTop, Category.assoc,
      Scheme.ΓSpecIso_naturality, ← Category.assoc, ← Scheme.toSpecΓ_appTop X.left,
      ← Scheme.Hom.comp_appTop, Scheme.toSpecΓ_isoSpec_inv, Scheme.Hom.id_appTop,
      Category.id_comp]
    rfl

lemma

homEquivAlgHom_smul

L209 ↗

AlgebraicGeometry.FiniteEtale.homEquivAlgHom_smul

Source context 8 commands

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

@[expose] public section
universe u
open CategoryTheory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ S)
variable (k K Ω : Type u) [Field k] [Field K] [Algebra k K] [Field Ω] [Algebra k Ω]
  [Algebra K Ω] [IsScalarTower k K Ω]
variable (X : FiniteEtale (Spec (.of k)))

Lean source · statement

lemma homEquivAlgHom_smul (X : FiniteEtale (Spec (.of k))) (g : K ≃ₐ[k] K) (x) :
    (homEquivAlgHom k K X) (g • x) = g • (homEquivAlgHom k K X x)

lemma

eq_one_of_smul_eq

L223 ↗

AlgebraicGeometry.FiniteEtale.eq_one_of_smul_eq

Source context 8 commands

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

@[expose] public section
universe u
open CategoryTheory
namespace AlgebraicGeometry
namespace FiniteEtale
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ S)
variable (k K Ω : Type u) [Field k] [Field K] [Algebra k K] [Field Ω] [Algebra k Ω]
  [Algebra K Ω] [IsScalarTower k K Ω]
variable (X : FiniteEtale (Spec (.of k)))

Lean source · statement

lemma eq_one_of_smul_eq [Algebra.IsSeparable k K] (g : K ≃ₐ[k] K)
    (H : ∀ (X : FiniteEtale (Spec (.of k))) (x : (Over.mk (ξ k K) ⟶ X.toComma)), g • x = x) :
    g = 1

Module documentation

Field-valued points and automorphism actions

Declarations