NYLL
Module

EtaleOverFieldEquivalence.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.EtaleOverFieldEquivalence
48 declarations indexed from sourceView source ↗

Module documentation

Étale schemes over a field and discrete Galois sets

This file assembles the finite Galois equivalence orbit by orbit. Its inverse sends a discrete continuous Galois set to the coproduct of the finite étale schemes corresponding to its finite orbits.

Imports9
Imported by1

Declarations

instance

(anonymous instance)

L38 ↗
Source context 6 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
Lean source · statement
instance : IsZariskiLocalAtSource
    (@AlgebraicGeometry.Etale : MorphismProperty Scheme.{u})
abbrev

G

L44 ↗
AlgebraicGeometry.Scheme.Etale.G
Source context 7 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
Lean source · statement
abbrev G
def

orbitQuotientEquivOfEquivariant

L48 ↗
AlgebraicGeometry.Scheme.Etale.orbitQuotientEquivOfEquivariant
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def orbitQuotientEquivOfEquivariant
    {H α β : Type u} [Group H] [MulAction H α] [MulAction H β]
    (e : α ≃ β) (he : ∀ (g : H) (x : α), e (g • x) = g • e x) :
    MulAction.orbitRel.Quotient H α ≃
      MulAction.orbitRel.Quotient H β
def

orbitEquivOfEquivariant

L61 ↗
AlgebraicGeometry.Scheme.Etale.orbitEquivOfEquivariant
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · full declaration
def orbitEquivOfEquivariant
    {H α β : Type u} [Group H] [MulAction H α] [MulAction H β]
    (e : α ≃ β) (he : ∀ (g : H) (x : α), e (g • x) = g • e x)
    (ω : MulAction.orbitRel.Quotient H α) :
    ω.orbit ≃ (orbitQuotientEquivOfEquivariant e he ω).orbit where
  toFun x := ⟨e x, by
    rw [MulAction.orbitRel.Quotient.mem_orbit]
    simpa only [orbitQuotientEquivOfEquivariant, Quotient.congr_mk] using
      congrArg (orbitQuotientEquivOfEquivariant e he)
        (MulAction.orbitRel.Quotient.mem_orbit.mp x.property)⟩
  invFun y := ⟨e.symm y, by
    rw [MulAction.orbitRel.Quotient.mem_orbit]
    apply (orbitQuotientEquivOfEquivariant e he).injective
    simpa only [orbitQuotientEquivOfEquivariant, Quotient.congr_mk,
      Equiv.apply_symm_apply] using
        MulAction.orbitRel.Quotient.mem_orbit.mp y.property⟩
  left_inv x := Subtype.ext (e.symm_apply_apply x)
  right_inv y := Subtype.ext (e.apply_symm_apply y)
lemma

orbitEquivOfEquivariant_smul

L80 ↗
AlgebraicGeometry.Scheme.Etale.orbitEquivOfEquivariant_smul
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
lemma orbitEquivOfEquivariant_smul
    {H α β : Type u} [Group H] [MulAction H α] [MulAction H β]
    (e : α ≃ β) (he : ∀ (g : H) (x : α), e (g • x) = g • e x)
    (ω : MulAction.orbitRel.Quotient H α) (g : H) (x : ω.orbit) :
    orbitEquivOfEquivariant e he ω (g • x) =
      g • orbitEquivOfEquivariant e he ω x
def

sigmaOrbitQuotientEquiv

L88 ↗
AlgebraicGeometry.Scheme.Etale.sigmaOrbitQuotientEquiv
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · full declaration
def sigmaOrbitQuotientEquiv
    {H ι : Type u} [Group H] (A : ι → Type u)
    [∀ i, MulAction H (A i)] [∀ i, MulAction.IsPretransitive H (A i)]
    [∀ i, Nonempty (A i)] :
    MulAction.orbitRel.Quotient H (Σ i, A i) ≃ ι where
  toFun := Quotient.lift Sigma.fst (by
    rintro ⟨i, a⟩ ⟨j, b⟩ ⟨g, h⟩
    simpa only [Sigma.smul_mk, Sigma.mk.injEq] using
      (congrArg Sigma.fst h).symm)
  invFun i := Quotient.mk'' ⟨i, Classical.arbitrary (A i)⟩
  left_inv ω := by
    induction ω using Quotient.inductionOn' with
    | _ x =>
      rcases x with ⟨i, x⟩
      rw [Quotient.eq'']
      obtain ⟨g, hg⟩ := MulAction.exists_smul_eq H x
        (Classical.arbitrary (A i))
      refine ⟨g, ?_⟩
      exact Sigma.ext rfl (heq_of_eq hg)
  right_inv i := rfl
def

sigmaOrbitEquivFiber

L109 ↗
AlgebraicGeometry.Scheme.Etale.sigmaOrbitEquivFiber
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · full declaration
def sigmaOrbitEquivFiber
    {H ι : Type u} [Group H] (A : ι → Type u)
    [∀ i, MulAction H (A i)] [∀ i, MulAction.IsPretransitive H (A i)]
    [∀ i, Nonempty (A i)]
    (ω : MulAction.orbitRel.Quotient H (Σ i, A i)) :
    ω.orbit ≃ A (sigmaOrbitQuotientEquiv A ω) where
  toFun x := by
    let h : x.1.1 = sigmaOrbitQuotientEquiv A ω := by
      have hx := MulAction.orbitRel.Quotient.mem_orbit.mp x.property
      exact congrArg (sigmaOrbitQuotientEquiv A) hx
    exact h ▸ x.1.2
  invFun a := ⟨⟨sigmaOrbitQuotientEquiv A ω, a⟩, by
    rw [MulAction.orbitRel.Quotient.mem_orbit]
    apply (sigmaOrbitQuotientEquiv A).injective
    rfl⟩
  left_inv x := by
    apply Subtype.ext
    rcases x with ⟨⟨i, x⟩, hx⟩
    have hi : i = sigmaOrbitQuotientEquiv A ω := by
      exact congrArg (sigmaOrbitQuotientEquiv A)
        (MulAction.orbitRel.Quotient.mem_orbit.mp hx)
    subst i
    rfl
  right_inv a := rfl
lemma

sigmaOrbitEquivFiber_smul

L134 ↗
AlgebraicGeometry.Scheme.Etale.sigmaOrbitEquivFiber_smul
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
lemma sigmaOrbitEquivFiber_smul
    {H ι : Type u} [Group H] (A : ι → Type u)
    [∀ i, MulAction H (A i)] [∀ i, MulAction.IsPretransitive H (A i)]
    [∀ i, Nonempty (A i)]
    (ω : MulAction.orbitRel.Quotient H (Σ i, A i))
    (g : H) (x : ω.orbit) :
    sigmaOrbitEquivFiber A ω (g • x) =
      g • sigmaOrbitEquivFiber A ω x
abbrev

finiteEtaleComponent

L149 ↗
AlgebraicGeometry.Scheme.Etale.finiteEtaleComponent
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · full declaration
abbrev finiteEtaleComponent
    {ι : Type u} (L : ι → CommRingCat.{u})
    (a : ∀ i, CommRingCat.of k ⟶ L i)
    (hField : ∀ i, IsField (L i))
    (hFiniteSep : ∀ i, letI := (a i).hom.toAlgebra
      Module.Finite k (L i) ∧ Algebra.IsSeparable k (L i))
    (i : ι) :
    AlgebraicGeometry.FiniteEtale (Spec (.of k)) := by
  letI : Field (L i) := (hField i).toField
  letI : Algebra k (L i) := (a i).hom.toAlgebra
  have hfs := hFiniteSep i
  letI : Module.Finite k (L i) := hfs.1
  letI : Algebra.IsSeparable k (L i) := hfs.2
  letI : Algebra.FormallyEtale k (L i) :=
    Algebra.FormallyEtale.of_isSeparable k (L i)
  letI : Module.FinitePresentation k (L i) :=
    Module.finitePresentation_of_finite k (L i)
  letI : Algebra.FinitePresentation k (L i) := inferInstance
  letI : Algebra.Etale k (L i) :=
    { formallyEtale := inferInstance
      finitePresentation := inferInstance }
  letI : Algebra.FiniteEtale k (L i) := ⟨⟩
  letI : IsFiniteEtale (Spec.map (a i)) := by
    rw [IsFiniteEtale.SpecMap_iff]
    change Algebra.FiniteEtale k (L i)
    infer_instance
  exact AlgebraicGeometry.FiniteEtale.mk (Spec.map (a i))
lemma

finiteEtaleComponent_hom

L178 ↗
AlgebraicGeometry.Scheme.Etale.finiteEtaleComponent_hom
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · full declaration
lemma finiteEtaleComponent_hom
    {ι : Type u} (L : ι → CommRingCat.{u})
    (a : ∀ i, CommRingCat.of k ⟶ L i)
    (hField : ∀ i, IsField (L i))
    (hFiniteSep : ∀ i, letI := (a i).hom.toAlgebra
      Module.Finite k (L i) ∧ Algebra.IsSeparable k (L i))
    (i : ι) :
    (finiteEtaleComponent k L a hField hFiniteSep i).hom = Spec.map (a i) :=
  rfl
theorem

finiteEtaleComponent_isConnected

L189 ↗
AlgebraicGeometry.Scheme.Etale.finiteEtaleComponent_isConnected
Source context 9 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
include K in
Lean source · full declaration
theorem finiteEtaleComponent_isConnected
    {ι : Type u} (L : ι → CommRingCat.{u})
    (a : ∀ i, CommRingCat.of k ⟶ L i)
    (hField : ∀ i, IsField (L i))
    (hFiniteSep : ∀ i, letI := (a i).hom.toAlgebra
      Module.Finite k (L i) ∧ Algebra.IsSeparable k (L i))
    (i : ι) :
    PreGaloisCategory.IsConnected
      (finiteEtaleComponent k L a hField hFiniteSep i) := by
  let : Field (L i) := (hField i).toField
  let : Algebra k (L i) := (a i).hom.toAlgebra
  have hfs := hFiniteSep i
  let : Module.Finite k (L i) := hfs.1
  let : Algebra.IsSeparable k (L i) := hfs.2
  let : Algebra.FormallyEtale k (L i) :=
    Algebra.FormallyEtale.of_isSeparable k (L i)
  let : Module.FinitePresentation k (L i) :=
    Module.finitePresentation_of_finite k (L i)
  let : Algebra.FinitePresentation k (L i) := inferInstance
  let : Algebra.Etale k (L i) :=
    { formallyEtale := inferInstance
      finitePresentation := inferInstance }
  let : Algebra.FiniteEtale k (L i) := ⟨⟩
  let : IsFiniteEtale (Spec.map (a i)) := by
    rw [IsFiniteEtale.SpecMap_iff]
    change Algebra.FiniteEtale k (L i)
    infer_instance
  change PreGaloisCategory.IsConnected
    (AlgebraicGeometry.FiniteEtale.mk (Spec.map (a i)))
  let Z := AlgebraicGeometry.FiniteEtale.mk (Spec.map (a i))
  constructor
  · apply (not_initial_iff_fiber_nonempty (fib k K) Z).mpr
    let φ : L i →ₐ[k] K := IsSepClosed.lift
    let x : Over.mk (ξ k K) ⟶ Z.toComma :=
      Over.homMk (Spec.map (CommRingCat.ofHom φ.toRingHom)) (by
        change Spec.map (CommRingCat.ofHom φ.toRingHom) ≫ Z.hom = ξ k K
        have hZhom : Z.hom = Spec.map (a i) := rfl
        have hring :
            a i ≫ CommRingCat.ofHom φ.toRingHom =
              CommRingCat.ofHom (algebraMap k K) := by
          ext z
          exact φ.commutes z
        rw [hZhom]
        exact (Spec.map_comp (a i)
          (CommRingCat.ofHom φ.toRingHom)).symm.trans
            (congrArg Spec.map hring))
    exact ⟨(AlgebraicGeometry.FiniteEtale.fiberObjEquivHom
      (ξ k K) Z).symm x⟩
  · intro Y j _ hj
    have hjOpen :
        IsOpenImmersion j.left :=
      ((AlgebraicGeometry.FiniteEtale.mono_iff (Spec (.of k)) Y Z j).mp
        (inferInstance : Mono j)).1
    let : IsOpenImmersion j.left := hjOpen
    have hFY :
        Nonempty ((fib k K).obj Y) :=
      (not_initial_iff_fiber_nonempty
        (fib k K) Y).mp hj
    let : Nonempty Y.left :=
      hFY.map AlgebraicGeometry.FiniteEtale.fiberPt
    let : Subsingleton Z.left := by
      change Subsingleton (PrimeSpectrum (L i))
      rw [PrimeSpectrum.subsingleton_iff_isField_of_isReduced]
      exact hField i
    have hjSurjective : Function.Surjective j.left := by
      intro z
      let y : Y.left := Classical.arbitrary Y.left
      exact ⟨y, Subsingleton.elim _ _⟩
    have hjRange : j.left.opensRange = ⊤ := by
      apply TopologicalSpace.Opens.ext
      rw [Scheme.Hom.coe_opensRange, TopologicalSpace.Opens.coe_top]
      exact Set.range_eq_univ.mpr hjSurjective
    let : IsIso j.left :=
      isIso_of_isOpenImmersion_of_opensRange_eq_top j.left hjRange
    exact AlgebraicGeometry.FiniteEtale.isIso_of_isIso_left j
lemma

sigmaOverHom_ext

L266 ↗
AlgebraicGeometry.Scheme.Etale.sigmaOverHom_ext
Source context 9 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
omit [IsSepClosure k K] in
Lean source · statement
lemma sigmaOverHom_ext
    {ι : Type u} (Z : ι → Over (Spec (.of k)))
    {q r : Σ i, (Over.mk (ξ k K) ⟶ Z i)}
    (h :
      (⟨q.1, q.2.left⟩ :
          Σ i, (Over.mk (ξ k K)).left ⟶ (Z i).left) =
        (⟨r.1, r.2.left⟩ :
          Σ i, (Over.mk (ξ k K)).left ⟶ (Z i).left)) :
    q = r
def

geometricFiberDecompositionEquiv

L284 ↗
AlgebraicGeometry.Scheme.Etale.geometricFiberDecompositionEquiv
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · full declaration
def geometricFiberDecompositionEquiv
    {ι : Type u} (X : (Spec (.of k)).Etale)
    (Z : ι → AlgebraicGeometry.FiniteEtale (Spec (.of k)))
    (e : (∐ fun i ↦ (Z i).left) ≅ X.left)
    (he : e.hom ≫ X.hom = Sigma.desc (fun i ↦ (Z i).hom)) :
    (Over.mk (ξ k K) ⟶ X.toComma) ≃
      Σ i, (Over.mk (ξ k K) ⟶ (Z i).toComma) where
  toFun x := by
    let q := Scheme.homSigmaEquiv (fun i ↦ (Z i).left)
      (Spec (.of K)) (x.left ≫ e.inv)
    refine ⟨q.1, Over.homMk q.2 ?_⟩
    change q.2 ≫ (Z q.1).hom = ξ k K
    have hq : q.2 ≫ Sigma.ι (fun i ↦ (Z i).left) q.1 =
        x.left ≫ e.inv := by
      dsimp only [q]
      rw [← Scheme.homSigmaEquiv_symm_apply]
      exact (Scheme.homSigmaEquiv (fun i ↦ (Z i).left)
        (Spec (.of K))).symm_apply_apply (x.left ≫ e.inv)
    have hx : x.left =
        (q.2 ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫ e.hom := by
      calc
        x.left = x.left ≫ (e.inv ≫ e.hom) := by
          rw [e.inv_hom_id, Category.comp_id]
        _ = (x.left ≫ e.inv) ≫ e.hom := (Category.assoc _ _ _).symm
        _ = (q.2 ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫ e.hom :=
          congrArg (fun m ↦ m ≫ e.hom) hq.symm
    let D : (∐ fun i ↦ (Z i).left) ⟶ Spec (.of k) :=
      Sigma.desc (fun i ↦ (Z i).hom)
    have hι :
        Sigma.ι (fun i ↦ (Z i).left) q.1 ≫ D = (Z q.1).hom :=
      Sigma.ι_comp_desc (fun i ↦ (Z i).hom) q.1
    have h1 :
        q.2 ≫ (Z q.1).hom =
          q.2 ≫ (Sigma.ι (fun i ↦ (Z i).left) q.1 ≫ D) :=
      congrArg (fun m ↦ q.2 ≫ m) hι.symm
    have h2 :
        q.2 ≫ (Sigma.ι (fun i ↦ (Z i).left) q.1 ≫ D) =
          (q.2 ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫ D :=
      (Category.assoc _ _ _).symm
    have h3 :
        (q.2 ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫ D =
          (q.2 ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫
            (e.hom ≫ X.hom) :=
      congrArg
        (fun m ↦
          (q.2 ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫ m)
        he.symm
    have h4 :
        (q.2 ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫
            (e.hom ≫ X.hom) =
          ((q.2 ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫ e.hom) ≫
            X.hom :=
      (Category.assoc _ _ _).symm
    have h5 :
        ((q.2 ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫ e.hom) ≫
            X.hom =
          x.left ≫ X.hom :=
      congrArg (fun m ↦ m ≫ X.hom) hx.symm
    exact h1.trans (h2.trans (h3.trans (h4.trans (h5.trans x.w))))
  invFun q := Over.homMk
    ((q.2.left ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫ e.hom) (by
      change ((q.2.left ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫ e.hom) ≫
        X.hom = ξ k K
      let D : (∐ fun i ↦ (Z i).left) ⟶ Spec (.of k) :=
        Sigma.desc (fun i ↦ (Z i).hom)
      have hι :
          Sigma.ι (fun i ↦ (Z i).left) q.1 ≫ D = (Z q.1).hom :=
        Sigma.ι_comp_desc (fun i ↦ (Z i).hom) q.1
      have h1 :
          ((q.2.left ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫ e.hom) ≫
              X.hom =
            (q.2.left ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫
              (e.hom ≫ X.hom) :=
        Category.assoc _ _ _
      have h2 :
          (q.2.left ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫
              (e.hom ≫ X.hom) =
            (q.2.left ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫ D :=
        congrArg
          (fun m ↦
            (q.2.left ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫ m) he
      have h3 :
          (q.2.left ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫ D =
            q.2.left ≫
              (Sigma.ι (fun i ↦ (Z i).left) q.1 ≫ D) :=
        Category.assoc _ _ _
      have h4 :
          q.2.left ≫
              (Sigma.ι (fun i ↦ (Z i).left) q.1 ≫ D) =
            q.2.left ≫ (Z q.1).hom :=
        congrArg (fun m ↦ q.2.left ≫ m) hι
      exact h1.trans (h2.trans (h3.trans (h4.trans q.2.w))))
  left_inv x := by
    dsimp only
    apply CategoryTheory.Over.OverMorphism.ext
    let q := Scheme.homSigmaEquiv (fun i ↦ (Z i).left)
      (Spec (.of K)) (x.left ≫ e.inv)
    have hq : q.2 ≫ Sigma.ι (fun i ↦ (Z i).left) q.1 =
        x.left ≫ e.inv := by
      dsimp only [q]
      rw [← Scheme.homSigmaEquiv_symm_apply]
      exact (Scheme.homSigmaEquiv (fun i ↦ (Z i).left)
        (Spec (.of K))).symm_apply_apply (x.left ≫ e.inv)
    calc
      (q.2 ≫ Sigma.ι (fun i ↦ (Z i).left) q.1) ≫ e.hom =
          (x.left ≫ e.inv) ≫ e.hom :=
        congrArg (fun m ↦ m ≫ e.hom) hq
      _ = x.left ≫ (e.inv ≫ e.hom) := Category.assoc _ _ _
      _ = x.left ≫ 𝟙 _ :=
        congrArg (fun m ↦ x.left ≫ m) e.inv_hom_id
      _ = x.left := Category.comp_id _
  right_inv q := by
    rcases q with ⟨i, y⟩
    let E := Scheme.homSigmaEquiv (fun j ↦ (Z j).left) (Spec (.of K))
    change
      (⟨(E ((((y.left ≫ Sigma.ι (fun j ↦ (Z j).left) i) ≫
          e.hom) ≫ e.inv))).1,
        CategoryTheory.Over.homMk
          (E ((((y.left ≫ Sigma.ι (fun j ↦ (Z j).left) i) ≫
            e.hom) ≫ e.inv))).2 _⟩ :
        Σ j, (Over.mk (ξ k K) ⟶ (Z j).toComma)) =
      (⟨i, y⟩ : Σ j, (Over.mk (ξ k K) ⟶ (Z j).toComma))
    have hs : (((y.left ≫ Sigma.ι (fun j ↦ (Z j).left) i) ≫
        e.hom) ≫ e.inv) =
        y.left ≫ Sigma.ι (fun j ↦ (Z j).left) i := by
      calc
        _ = (y.left ≫ Sigma.ι (fun j ↦ (Z j).left) i) ≫
              (e.hom ≫ e.inv) := Category.assoc _ _ _
        _ = (y.left ≫ Sigma.ι (fun j ↦ (Z j).left) i) ≫ 𝟙 _ :=
          congrArg (fun m ↦
            (y.left ≫ Sigma.ι (fun j ↦ (Z j).left) i) ≫ m)
            e.hom_inv_id
        _ = _ := Category.comp_id _
    have hr :
        E ((((y.left ≫ Sigma.ι (fun j ↦ (Z j).left) i) ≫
          e.hom) ≫ e.inv)) = ⟨i, y.left⟩ := by
      calc
        E ((((y.left ≫ Sigma.ι (fun j ↦ (Z j).left) i) ≫
            e.hom) ≫ e.inv)) =
            E (y.left ≫ Sigma.ι (fun j ↦ (Z j).left) i) :=
          congrArg E hs
        _ = ⟨i, y.left⟩ := by
          have h := E.apply_symm_apply ⟨i, y.left⟩
          rw [Scheme.homSigmaEquiv_symm_apply] at h
          exact h
    apply sigmaOverHom_ext k K (fun j ↦ (Z j).toComma)
    exact hr
lemma

geometricFiberDecompositionEquiv_rho

L433 ↗
AlgebraicGeometry.Scheme.Etale.geometricFiberDecompositionEquiv_rho
Source context 9 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
omit [IsSepClosure k K] in
Lean source · full declaration
lemma geometricFiberDecompositionEquiv_rho
    {ι : Type u} (X : (Spec (.of k)).Etale)
    (Z : ι → AlgebraicGeometry.FiniteEtale (Spec (.of k)))
    (e : (∐ fun i ↦ (Z i).left) ≅ X.left)
    (he : e.hom ≫ X.hom = Sigma.desc (fun i ↦ (Z i).hom))
    (g : G k K) (x : Over.mk (ξ k K) ⟶ X.toComma) :
    geometricFiberDecompositionEquiv k K X Z e he
        (ConcreteCategory.hom
          (((geometricFiber k K).obj X).obj.obj.ρ g) x) =
      g • geometricFiberDecompositionEquiv k K X Z e he x := by
  let σ : Spec (.of K) ⟶ Spec (.of K) :=
    Spec.map (CommRingCat.ofHom (g : K →+* K))
  let q := Scheme.homSigmaEquiv (fun i ↦ (Z i).left)
    (Spec (.of K)) (x.left ≫ e.inv)
  let xg : Over.mk (ξ k K) ⟶ X.toComma :=
    ConcreteCategory.hom
      (((geometricFiber k K).obj X).obj.obj.ρ g) x
  let qg := Scheme.homSigmaEquiv (fun i ↦ (Z i).left)
    (Spec (.of K)) (xg.left ≫ e.inv)
  have hxg : xg.left ≫ e.inv = σ ≫ (x.left ≫ e.inv) := by
    change
      (Spec.map (CommRingCat.ofHom (g : K →+* K)) ≫ x.left) ≫ e.inv =
        σ ≫ (x.left ≫ e.inv)
    dsimp only [σ]
    exact Category.assoc _ _ _
  have hqg : qg = ⟨q.1, σ ≫ q.2⟩ := by
    dsimp only [qg, q]
    calc
      Scheme.homSigmaEquiv (fun i ↦ (Z i).left) (Spec (.of K))
          (xg.left ≫ e.inv) =
          Scheme.homSigmaEquiv (fun i ↦ (Z i).left) (Spec (.of K))
            (σ ≫ (x.left ≫ e.inv)) :=
        congrArg
          (Scheme.homSigmaEquiv (fun i ↦ (Z i).left) (Spec (.of K))) hxg
      _ = ⟨(Scheme.homSigmaEquiv (fun i ↦ (Z i).left)
              (Spec (.of K)) (x.left ≫ e.inv)).1,
            σ ≫ (Scheme.homSigmaEquiv (fun i ↦ (Z i).left)
              (Spec (.of K)) (x.left ≫ e.inv)).2⟩ :=
        Scheme.homSigmaEquiv_comp (fun i ↦ (Z i).left)
          σ (x.left ≫ e.inv)
  apply sigmaOverHom_ext k K (fun i ↦ (Z i).toComma)
  change qg = ⟨q.1, σ ≫ q.2⟩
  exact hqg
def

orbitIndexMap

L478 ↗
AlgebraicGeometry.Scheme.Etale.orbitIndexMap
Documentation

The map on orbit sets induced by an equivariant map.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def orbitIndexMap
    {S T : DiscreteContAction TopCat (G k K)} (f : S ⟶ T) :
    MulAction.orbitRel.Quotient (G k K)
        ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) →
      MulAction.orbitRel.Quotient (G k K)
        ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj T)
def

orbitMap

L492 ↗
AlgebraicGeometry.Scheme.Etale.orbitMap
Documentation

Restriction of an equivariant map to one source orbit.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def orbitMap
    {S T : DiscreteContAction TopCat (G k K)} (f : S ⟶ T)
    (ω : MulAction.orbitRel.Quotient (G k K)
      ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S)) :
    ω.orbit → (orbitIndexMap k K f ω).orbit
def

orbitContActionMap

L507 ↗
AlgebraicGeometry.Scheme.Etale.orbitContActionMap
Documentation

Restriction of an equivariant map to one source orbit, bundled as a morphism of finite continuous actions.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def orbitContActionMap
    {S T : DiscreteContAction TopCat (G k K)} (f : S ⟶ T)
    (ω : MulAction.orbitRel.Quotient (G k K)
      ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S)) :
    DiscreteContAction.orbitContAction S ω ⟶
      DiscreteContAction.orbitContAction T (orbitIndexMap k K f ω)
abbrev

orbitFiniteEtale

L521 ↗
AlgebraicGeometry.Scheme.Etale.orbitFiniteEtale
Documentation

The finite étale scheme corresponding to one orbit.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
abbrev orbitFiniteEtale
    (S : DiscreteContAction TopCat (G k K))
    (ω : MulAction.orbitRel.Quotient (G k K)
      ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S)) :
    AlgebraicGeometry.FiniteEtale (Spec (.of k))
abbrev

orbitFiniteEtaleMap

L531 ↗
AlgebraicGeometry.Scheme.Etale.orbitFiniteEtaleMap
Documentation

The finite étale morphism corresponding to the restriction of an equivariant map to one orbit.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
abbrev orbitFiniteEtaleMap
    {S T : DiscreteContAction TopCat (G k K)} (f : S ⟶ T)
    (ω : MulAction.orbitRel.Quotient (G k K)
      ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S)) :
    orbitFiniteEtale k K S ω ⟶
      orbitFiniteEtale k K T (orbitIndexMap k K f ω)
abbrev

inverseObj

L542 ↗
AlgebraicGeometry.Scheme.Etale.inverseObj
Documentation

Object part of the inverse in Tag 03QR: take the coproduct of the finite étale schemes attached to all orbits.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
abbrev inverseObj
    (S : DiscreteContAction TopCat (G k K)) :
    (Spec (.of k)).Etale
lemma

inverseObj_hom

L556 ↗
AlgebraicGeometry.Scheme.Etale.inverseObj_hom
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · full declaration
lemma inverseObj_hom
    (S : DiscreteContAction TopCat (G k K)) :
    (inverseObj k K S).hom =
      Sigma.desc (fun ω : MulAction.orbitRel.Quotient (G k K)
          ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
        (orbitFiniteEtale k K S ω).hom) :=
  rfl
abbrev

inverseMap

L566 ↗
AlgebraicGeometry.Scheme.Etale.inverseMap
Documentation

Morphism part of the inverse: each source orbit is sent into the orbit containing its image, then the finite Galois equivalence is applied.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
abbrev inverseMap
    {S T : DiscreteContAction TopCat (G k K)} (f : S ⟶ T) :
    inverseObj k K S ⟶ inverseObj k K T
lemma

inverseMap_left

L629 ↗
AlgebraicGeometry.Scheme.Etale.inverseMap_left
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · full declaration
lemma inverseMap_left
    {S T : DiscreteContAction TopCat (G k K)} (f : S ⟶ T) :
    (inverseMap k K f).left =
      Sigma.desc (fun ω ↦
        (orbitFiniteEtaleMap k K f ω).left ≫
          Sigma.ι
            (fun η : MulAction.orbitRel.Quotient (G k K)
                ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj T) ↦
              (orbitFiniteEtale k K T η).left)
            (orbitIndexMap k K f ω)) :=
  rfl
abbrev

inverseFunctor

L642 ↗
AlgebraicGeometry.Scheme.Etale.inverseFunctor
Documentation

The orbitwise-coproduct inverse functor.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · full declaration
abbrev inverseFunctor :
    DiscreteContAction TopCat (G k K) ⥤ (Spec (.of k)).Etale where
  obj := inverseObj k K
  map := inverseMap k K
  map_id S := by
    apply MorphismProperty.Over.Hom.ext
    apply Sigma.hom_ext
    intro ω
    induction ω using Quotient.inductionOn'
    rename_i a
    let Y := fun η : MulAction.orbitRel.Quotient (G k K)
        ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
      (orbitFiniteEtale k K S η).left
    have hι :
        Sigma.ι Y (Quotient.mk'' a) ≫ (inverseMap k K (𝟙 S)).left =
          (orbitFiniteEtaleMap k K (𝟙 S) (Quotient.mk'' a)).left ≫
            Sigma.ι Y (Quotient.mk'' a) := by
      rw [inverseMap_left]
      exact Sigma.ι_comp_desc _ _
    have hm : orbitContActionMap k K (𝟙 S) (Quotient.mk'' a) = 𝟙 _ := by
      apply ObjectProperty.hom_ext
      apply Action.hom_ext
      ext x
      rfl
    have hf :
        orbitFiniteEtaleMap k K (𝟙 S) (Quotient.mk'' a) = 𝟙 _ := by
      change
        (AlgebraicGeometry.FiniteEtale.equivContAction k K).inverse.map
            (orbitContActionMap k K (𝟙 S) (Quotient.mk'' a)) =
          𝟙 _
      rw [hm]
      exact CategoryTheory.Functor.map_id _ _
    rw [hf] at hι
    have hidSource :
        (𝟙 (orbitFiniteEtale k K S (Quotient.mk'' a)) :
          orbitFiniteEtale k K S (Quotient.mk'' a) ⟶
            orbitFiniteEtale k K S (Quotient.mk'' a)).left = 𝟙 _ := rfl
    have hidTarget :
        (𝟙 (inverseObj k K S) :
          inverseObj k K S ⟶ inverseObj k K S).left = 𝟙 _ := rfl
    have hsource :
        (𝟙 (orbitFiniteEtale k K S (Quotient.mk'' a)) :
            orbitFiniteEtale k K S (Quotient.mk'' a) ⟶
              orbitFiniteEtale k K S (Quotient.mk'' a)).left ≫
            Sigma.ι Y (Quotient.mk'' a) =
          Sigma.ι Y (Quotient.mk'' a) := by
      calc
        _ = 𝟙 _ ≫ Sigma.ι Y (Quotient.mk'' a) :=
          congrArg (fun t ↦ t ≫ Sigma.ι Y (Quotient.mk'' a)) hidSource
        _ = _ := Category.id_comp _
    have htarget :
        Sigma.ι Y (Quotient.mk'' a) ≫
            (𝟙 (inverseObj k K S) :
              inverseObj k K S ⟶ inverseObj k K S).left =
          Sigma.ι Y (Quotient.mk'' a) := by
      calc
        _ = Sigma.ι Y (Quotient.mk'' a) ≫ 𝟙 _ :=
          congrArg (fun t ↦ Sigma.ι Y (Quotient.mk'' a) ≫ t) hidTarget
        _ = _ := Category.comp_id _
    exact hι.trans (hsource.trans htarget.symm)
  map_comp f g := by
    rename_i S T U
    apply MorphismProperty.Over.Hom.ext
    apply Sigma.hom_ext
    intro ω
    induction ω using Quotient.inductionOn'
    rename_i a
    let YS := fun η : MulAction.orbitRel.Quotient (G k K)
        ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
      (orbitFiniteEtale k K S η).left
    let YT := fun η : MulAction.orbitRel.Quotient (G k K)
        ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj T) ↦
      (orbitFiniteEtale k K T η).left
    let YU := fun η : MulAction.orbitRel.Quotient (G k K)
        ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj U) ↦
      (orbitFiniteEtale k K U η).left
    have hιf :
        Sigma.ι YS (Quotient.mk'' a) ≫ (inverseMap k K f).left =
          (orbitFiniteEtaleMap k K f (Quotient.mk'' a)).left ≫
            Sigma.ι YT (orbitIndexMap k K f (Quotient.mk'' a)) := by
      rw [inverseMap_left]
      exact Sigma.ι_comp_desc _ _
    have hιg :
        Sigma.ι YT (orbitIndexMap k K f (Quotient.mk'' a)) ≫
            (inverseMap k K g).left =
          (orbitFiniteEtaleMap k K g
              (orbitIndexMap k K f (Quotient.mk'' a))).left ≫
            Sigma.ι YU
              (orbitIndexMap k K g
                (orbitIndexMap k K f (Quotient.mk'' a))) := by
      rw [inverseMap_left]
      exact Sigma.ι_comp_desc _ _
    have hιfg :
        Sigma.ι YS (Quotient.mk'' a) ≫ (inverseMap k K (f ≫ g)).left =
          (orbitFiniteEtaleMap k K (f ≫ g) (Quotient.mk'' a)).left ≫
            Sigma.ι YU
              (orbitIndexMap k K (f ≫ g) (Quotient.mk'' a)) := by
      rw [inverseMap_left]
      exact Sigma.ι_comp_desc _ _
    have hm :
        orbitContActionMap k K (f ≫ g) (Quotient.mk'' a) =
          orbitContActionMap k K f (Quotient.mk'' a) ≫
            orbitContActionMap k K g
              (orbitIndexMap k K f (Quotient.mk'' a)) := by
      apply ObjectProperty.hom_ext
      apply Action.hom_ext
      ext x
      rfl
    have hf :
        orbitFiniteEtaleMap k K (f ≫ g) (Quotient.mk'' a) =
          orbitFiniteEtaleMap k K f (Quotient.mk'' a) ≫
            orbitFiniteEtaleMap k K g
              (orbitIndexMap k K f (Quotient.mk'' a)) := by
      change
        (AlgebraicGeometry.FiniteEtale.equivContAction k K).inverse.map
            (orbitContActionMap k K (f ≫ g) (Quotient.mk'' a)) =
          (AlgebraicGeometry.FiniteEtale.equivContAction k K).inverse.map
              (orbitContActionMap k K f (Quotient.mk'' a)) ≫
            (AlgebraicGeometry.FiniteEtale.equivContAction k K).inverse.map
              (orbitContActionMap k K g
                (orbitIndexMap k K f (Quotient.mk'' a)))
      rw [hm]
      exact CategoryTheory.Functor.map_comp _ _ _
    have hright :
        Sigma.ι YS (Quotient.mk'' a) ≫
            ((inverseMap k K f).left ≫ (inverseMap k K g).left) =
          ((orbitFiniteEtaleMap k K f (Quotient.mk'' a)).left ≫
            (orbitFiniteEtaleMap k K g
              (orbitIndexMap k K f (Quotient.mk'' a))).left) ≫
            Sigma.ι YU
              (orbitIndexMap k K g
                (orbitIndexMap k K f (Quotient.mk'' a))) := by
      calc
        _ = (Sigma.ι YS (Quotient.mk'' a) ≫
              (inverseMap k K f).left) ≫ (inverseMap k K g).left :=
            (Category.assoc _ _ _).symm
        _ = ((orbitFiniteEtaleMap k K f (Quotient.mk'' a)).left ≫
              Sigma.ι YT (orbitIndexMap k K f (Quotient.mk'' a))) ≫
              (inverseMap k K g).left :=
            congrArg (fun t ↦ t ≫ (inverseMap k K g).left) hιf
        _ = _ := by
            let u := (orbitFiniteEtaleMap k K f (Quotient.mk'' a)).left
            let v := Sigma.ι YT (orbitIndexMap k K f (Quotient.mk'' a))
            let w := (inverseMap k K g).left
            let z := (orbitFiniteEtaleMap k K g
              (orbitIndexMap k K f (Quotient.mk'' a))).left
            let j := Sigma.ι YU
              (orbitIndexMap k K g
                (orbitIndexMap k K f (Quotient.mk'' a)))
            have h₁ : (u ≫ v) ≫ w = u ≫ (v ≫ w) := Category.assoc _ _ _
            have h₂ : u ≫ (v ≫ w) = u ≫ (z ≫ j) :=
              congrArg (fun t ↦ u ≫ t) hιg
            have h₃ : u ≫ (z ≫ j) = (u ≫ z) ≫ j :=
              (Category.assoc _ _ _).symm
            exact h₁.trans (h₂.trans h₃)
    rw [hf] at hιfg
    change
      Sigma.ι YS (Quotient.mk'' a) ≫ (inverseMap k K (f ≫ g)).left =
        Sigma.ι YS (Quotient.mk'' a) ≫
          ((inverseMap k K f).left ≫ (inverseMap k K g).left)
    simpa only [MorphismProperty.Comma.comp_left] using hιfg.trans hright.symm
def

inverseObjGeometricFiberEquiv

L806 ↗
AlgebraicGeometry.Scheme.Etale.inverseObjGeometricFiberEquiv
Documentation

A geometric point of the coproduct defining inverseObj is uniquely a geometric point of one orbit summand.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · full declaration
def inverseObjGeometricFiberEquiv
    (S : DiscreteContAction TopCat (G k K)) :
    (Over.mk (ξ k K) ⟶ (inverseObj k K S).toComma) ≃
      Σ ω : MulAction.orbitRel.Quotient (G k K)
        ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S),
        (Over.mk (ξ k K) ⟶ (orbitFiniteEtale k K S ω).toComma) where
  toFun x := by
    let q := Scheme.homSigmaEquiv
      (fun ω : MulAction.orbitRel.Quotient (G k K)
          ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
        (orbitFiniteEtale k K S ω).left) (Spec (.of K)) x.left
    refine ⟨q.1, Over.homMk q.2 ?_⟩
    change q.2 ≫ (orbitFiniteEtale k K S q.1).hom = ξ k K
    have hx := x.w
    change x.left ≫ Sigma.desc
      (fun ω : MulAction.orbitRel.Quotient (G k K)
          ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
        (orbitFiniteEtale k K S ω).hom) = ξ k K at hx
    have hq : q.2 ≫ Sigma.ι
        (fun ω : MulAction.orbitRel.Quotient (G k K)
            ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
          (orbitFiniteEtale k K S ω).left) q.1 = x.left := by
      simpa only [q, Scheme.homSigmaEquiv_symm_apply] using
        (Scheme.homSigmaEquiv
          (fun ω : MulAction.orbitRel.Quotient (G k K)
              ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
            (orbitFiniteEtale k K S ω).left)
          (Spec (.of K))).symm_apply_apply x.left
    let D :
        (∐ fun ω : MulAction.orbitRel.Quotient (G k K)
            ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
          (orbitFiniteEtale k K S ω).left) ⟶ Spec (.of k) :=
      Sigma.desc
        (fun ω : MulAction.orbitRel.Quotient (G k K)
            ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
          (orbitFiniteEtale k K S ω).hom)
    have hι :
        Sigma.ι
            (fun ω : MulAction.orbitRel.Quotient (G k K)
                ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
              (orbitFiniteEtale k K S ω).left) q.1 ≫ D =
          (orbitFiniteEtale k K S q.1).hom :=
      Sigma.ι_comp_desc
        (fun ω : MulAction.orbitRel.Quotient (G k K)
            ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
          (orbitFiniteEtale k K S ω).hom) q.1
    have h1 :
        q.2 ≫ (orbitFiniteEtale k K S q.1).hom =
          q.2 ≫
            (Sigma.ι
                (fun ω : MulAction.orbitRel.Quotient (G k K)
                    ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
                  (orbitFiniteEtale k K S ω).left) q.1 ≫ D) :=
      congrArg (fun m ↦ q.2 ≫ m) hι.symm
    have h2 :
        q.2 ≫
            (Sigma.ι
                (fun ω : MulAction.orbitRel.Quotient (G k K)
                    ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
                  (orbitFiniteEtale k K S ω).left) q.1 ≫ D) =
          (q.2 ≫ Sigma.ι
            (fun ω : MulAction.orbitRel.Quotient (G k K)
                ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
              (orbitFiniteEtale k K S ω).left) q.1) ≫ D :=
      (Category.assoc _ _ _).symm
    have h3 :
        (q.2 ≫ Sigma.ι
            (fun ω : MulAction.orbitRel.Quotient (G k K)
                ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
              (orbitFiniteEtale k K S ω).left) q.1) ≫ D =
          x.left ≫ D :=
      congrArg (fun m ↦ m ≫ D) hq
    exact h1.trans (h2.trans (h3.trans hx))
  invFun q := Over.homMk
    (q.2.left ≫ Sigma.ι
      (fun ω : MulAction.orbitRel.Quotient (G k K)
          ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
        (orbitFiniteEtale k K S ω).left) q.1) (by
      change (q.2.left ≫ Sigma.ι
        (fun ω : MulAction.orbitRel.Quotient (G k K)
            ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
          (orbitFiniteEtale k K S ω).left) q.1) ≫
        Sigma.desc
          (fun ω : MulAction.orbitRel.Quotient (G k K)
              ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
            (orbitFiniteEtale k K S ω).hom) = ξ k K
      let D :
          (∐ fun ω : MulAction.orbitRel.Quotient (G k K)
              ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
            (orbitFiniteEtale k K S ω).left) ⟶ Spec (.of k) :=
        Sigma.desc
          (fun ω : MulAction.orbitRel.Quotient (G k K)
              ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
            (orbitFiniteEtale k K S ω).hom)
      have hι :
          Sigma.ι
              (fun ω : MulAction.orbitRel.Quotient (G k K)
                  ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
                (orbitFiniteEtale k K S ω).left) q.1 ≫ D =
            (orbitFiniteEtale k K S q.1).hom :=
        Sigma.ι_comp_desc
          (fun ω : MulAction.orbitRel.Quotient (G k K)
              ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
            (orbitFiniteEtale k K S ω).hom) q.1
      have h1 :
          (q.2.left ≫ Sigma.ι
            (fun ω : MulAction.orbitRel.Quotient (G k K)
                ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
              (orbitFiniteEtale k K S ω).left) q.1) ≫ D =
            q.2.left ≫
              (Sigma.ι
                (fun ω : MulAction.orbitRel.Quotient (G k K)
                    ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
                  (orbitFiniteEtale k K S ω).left) q.1 ≫ D) :=
        Category.assoc _ _ _
      have h2 :
          q.2.left ≫
              (Sigma.ι
                (fun ω : MulAction.orbitRel.Quotient (G k K)
                    ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
                  (orbitFiniteEtale k K S ω).left) q.1 ≫ D) =
            q.2.left ≫ (orbitFiniteEtale k K S q.1).hom :=
        congrArg (fun m ↦ q.2.left ≫ m) hι
      exact h1.trans (h2.trans q.2.w))
  left_inv x := by
    dsimp only
    apply CategoryTheory.Over.OverMorphism.ext
    let q := Scheme.homSigmaEquiv
      (fun ω : MulAction.orbitRel.Quotient (G k K)
          ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
        (orbitFiniteEtale k K S ω).left) (Spec (.of K)) x.left
    change q.2 ≫ Sigma.ι
      (fun ω : MulAction.orbitRel.Quotient (G k K)
          ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
        (orbitFiniteEtale k K S ω).left) q.1 = x.left
    simpa only [q, Scheme.homSigmaEquiv_symm_apply] using
      (Scheme.homSigmaEquiv
        (fun ω : MulAction.orbitRel.Quotient (G k K)
            ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
          (orbitFiniteEtale k K S ω).left)
        (Spec (.of K))).symm_apply_apply x.left
  right_inv q := by
    rcases q with ⟨ω, y⟩
    let Y := fun η : MulAction.orbitRel.Quotient (G k K)
        ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S) ↦
      (orbitFiniteEtale k K S η).left
    let E := Scheme.homSigmaEquiv Y (Spec (.of K))
    change
      (⟨(E (y.left ≫ Sigma.ι Y ω)).1,
        CategoryTheory.Over.homMk (E (y.left ≫ Sigma.ι Y ω)).2 _⟩ :
        Σ η : MulAction.orbitRel.Quotient (G k K)
            ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S),
          (Over.mk (ξ k K) ⟶ (orbitFiniteEtale k K S η).toComma)) =
      (⟨ω, y⟩ :
        Σ η : MulAction.orbitRel.Quotient (G k K)
            ((forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S),
          (Over.mk (ξ k K) ⟶ (orbitFiniteEtale k K S η).toComma))
    have hr : E (y.left ≫ Sigma.ι Y ω) = ⟨ω, y.left⟩ := by
      have h := E.apply_symm_apply ⟨ω, y.left⟩
      rw [Scheme.homSigmaEquiv_symm_apply] at h
      exact h
    apply sigmaOverHom_ext k K
      (fun η ↦ (orbitFiniteEtale k K S η).toComma)
    exact hr
def

finiteCounitEquiv

L973 ↗
AlgebraicGeometry.Scheme.Etale.finiteCounitEquiv
Documentation

The underlying bijection supplied by the counit of the finite Galois equivalence.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def finiteCounitEquiv
    (A : ContAction FintypeCat (G k K)) :
    (forget₂ (ContAction FintypeCat (G k K)) FintypeCat).obj
        ((AlgebraicGeometry.FiniteEtale.equivContAction k K).functor.obj
          ((AlgebraicGeometry.FiniteEtale.equivContAction k K).inverse.obj A)) ≃
      (forget₂ (ContAction FintypeCat (G k K)) FintypeCat).obj A
def

finiteGeometricFiberEquiv

L985 ↗
AlgebraicGeometry.Scheme.Etale.finiteGeometricFiberEquiv
Documentation

On a finite orbit, the finite Galois equivalence identifies the geometric fiber of the corresponding finite étale scheme with that orbit.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def finiteGeometricFiberEquiv
    (A : ContAction FintypeCat (G k K)) :
    (Over.mk (ξ k K) ⟶
      ((AlgebraicGeometry.FiniteEtale.equivContAction k K).inverse.obj A).toComma) ≃
      (forget₂ (ContAction FintypeCat (G k K)) FintypeCat).obj A
lemma

finiteGeometricFiberEquiv_smul

L994 ↗
AlgebraicGeometry.Scheme.Etale.finiteGeometricFiberEquiv_smul
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
lemma finiteGeometricFiberEquiv_smul
    (A : ContAction FintypeCat (G k K)) (g : G k K)
    (x : Over.mk (ξ k K) ⟶
      ((AlgebraicGeometry.FiniteEtale.equivContAction k K).inverse.obj A).toComma) :
    finiteGeometricFiberEquiv k K A (g • x) =
      ConcreteCategory.hom (A.obj.ρ g)
        (finiteGeometricFiberEquiv k K A x)
lemma

finiteGeometricFiberEquiv_naturality

L1021 ↗
AlgebraicGeometry.Scheme.Etale.finiteGeometricFiberEquiv_naturality
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
lemma finiteGeometricFiberEquiv_naturality
    {A B : ContAction FintypeCat (G k K)} (f : A ⟶ B)
    (x : Over.mk (ξ k K) ⟶
      ((AlgebraicGeometry.FiniteEtale.equivContAction k K).inverse.obj A).toComma) :
    finiteGeometricFiberEquiv k K B
        (x ≫ ((AlgebraicGeometry.FiniteEtale.equivContAction k K).inverse.map f).hom) =
      f.hom.hom (finiteGeometricFiberEquiv k K A x)
def

inverseObjCounitEquiv

L1043 ↗
AlgebraicGeometry.Scheme.Etale.inverseObjCounitEquiv
Documentation

The objectwise counit bijection: split a geometric point by its unique orbit summand, use the finite counit on that summand, then reassemble the orbits.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def inverseObjCounitEquiv
    (S : DiscreteContAction TopCat (G k K)) :
    (Over.mk (ξ k K) ⟶ (inverseObj k K S).toComma) ≃
      (forget₂ (DiscreteContAction TopCat (G k K)) TopCat).obj S
lemma

inverseObjGeometricFiberEquiv_rho

L1054 ↗
AlgebraicGeometry.Scheme.Etale.inverseObjGeometricFiberEquiv_rho
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
lemma inverseObjGeometricFiberEquiv_rho
    (S : DiscreteContAction TopCat (G k K)) (g : G k K)
    (x : Over.mk (ξ k K) ⟶ (inverseObj k K S).toComma) :
    inverseObjGeometricFiberEquiv k K S
        (ConcreteCategory.hom
          (((geometricFiber k K).obj (inverseObj k K S)).obj.obj.ρ g) x) =
      ⟨(inverseObjGeometricFiberEquiv k K S x).1,
        g • (inverseObjGeometricFiberEquiv k K S x).2⟩
lemma

inverseObjGeometricFiberEquiv_map

L1092 ↗
AlgebraicGeometry.Scheme.Etale.inverseObjGeometricFiberEquiv_map
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
lemma inverseObjGeometricFiberEquiv_map
    {S T : DiscreteContAction TopCat (G k K)} (f : S ⟶ T)
    (x : Over.mk (ξ k K) ⟶ (inverseObj k K S).toComma) :
    inverseObjGeometricFiberEquiv k K T
        ((geometricFiber k K).map (inverseMap k K f) x) =
      ⟨orbitIndexMap k K f (inverseObjGeometricFiberEquiv k K S x).1,
        (inverseObjGeometricFiberEquiv k K S x).2 ≫
          (orbitFiniteEtaleMap k K f
            (inverseObjGeometricFiberEquiv k K S x).1).hom⟩
lemma

inverseObjCounitEquiv_rho

L1156 ↗
AlgebraicGeometry.Scheme.Etale.inverseObjCounitEquiv_rho
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
lemma inverseObjCounitEquiv_rho
    (S : DiscreteContAction TopCat (G k K)) (g : G k K)
    (x : Over.mk (ξ k K) ⟶ (inverseObj k K S).toComma) :
    inverseObjCounitEquiv k K S
        (ConcreteCategory.hom
          (((geometricFiber k K).obj (inverseObj k K S)).obj.obj.ρ g) x) =
      g • inverseObjCounitEquiv k K S x
lemma

inverseObjCounitEquiv_naturality

L1190 ↗
AlgebraicGeometry.Scheme.Etale.inverseObjCounitEquiv_naturality
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
lemma inverseObjCounitEquiv_naturality
    {S T : DiscreteContAction TopCat (G k K)} (f : S ⟶ T)
    (x : Over.mk (ξ k K) ⟶ (inverseObj k K S).toComma) :
    inverseObjCounitEquiv k K T
        ((geometricFiber k K).map (inverseMap k K f) x) =
      f.hom.hom.hom (inverseObjCounitEquiv k K S x)
def

inverseObjCounitIso

L1228 ↗
AlgebraicGeometry.Scheme.Etale.inverseObjCounitIso
Documentation

The objectwise counit is an isomorphism of discrete continuous actions.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def inverseObjCounitIso
    (S : DiscreteContAction TopCat (G k K)) :
    (geometricFiber k K).obj (inverseObj k K S) ≅ S
def

inverseCounitIso

L1255 ↗
AlgebraicGeometry.Scheme.Etale.inverseCounitIso
Documentation

The orbitwise inverse followed by the geometric-fiber functor is naturally isomorphic to the identity.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def inverseCounitIso :
    inverseFunctor k K ⋙ geometricFiber k K ≅
      𝟭 (DiscreteContAction TopCat (G k K))
def

uncorrectedUnitObjIso

L1267 ↗
AlgebraicGeometry.Scheme.Etale.uncorrectedUnitObjIso
Documentation

Before imposing naturality, the component decomposition of an étale scheme identifies it with the orbitwise inverse of its geometric fiber.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def uncorrectedUnitObjIso
    (X : (Spec (.of k)).Etale) :
    inverseObj k K ((geometricFiber k K).obj X) ≅ X
lemma

geometricFiber_map_injective

L1461 ↗
AlgebraicGeometry.Scheme.Etale.geometricFiber_map_injective
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
lemma geometricFiber_map_injective
    {X Y : (Spec (.of k)).Etale} {f g : X ⟶ Y}
    (h : (geometricFiber k K).map f = (geometricFiber k K).map g) :
    f = g
instance

geometricFiberFaithful

L1532 ↗
AlgebraicGeometry.Scheme.Etale.geometricFiberFaithful
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · full declaration
instance geometricFiberFaithful :
    (geometricFiber k K).Faithful where
  map_injective h := geometricFiber_map_injective k K h
def

geometricFiberCounitComponent

L1536 ↗
AlgebraicGeometry.Scheme.Etale.geometricFiberCounitComponent
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def geometricFiberCounitComponent
    (S : DiscreteContAction TopCat (G k K)) :
    (geometricFiber k K).obj ((inverseFunctor k K).obj S) ≅ S
lemma

geometricFiberCounitComponent_naturality

L1541 ↗
AlgebraicGeometry.Scheme.Etale.geometricFiberCounitComponent_naturality
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
lemma geometricFiberCounitComponent_naturality
    {S T : DiscreteContAction TopCat (G k K)} (f : S ⟶ T) :
    (geometricFiber k K).map ((inverseFunctor k K).map f) ≫
        (geometricFiberCounitComponent k K T).hom =
      (geometricFiberCounitComponent k K S).hom ≫ f
def

unitDefect

L1548 ↗
AlgebraicGeometry.Scheme.Etale.unitDefect
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def unitDefect
    (X : (Spec (.of k)).Etale) :
    (geometricFiber k K).obj X ≅ (geometricFiber k K).obj X
def

unitComponent

L1555 ↗
AlgebraicGeometry.Scheme.Etale.unitComponent
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def unitComponent
    (X : (Spec (.of k)).Etale) :
    X ≅ (inverseFunctor k K).obj ((geometricFiber k K).obj X)
lemma

unitComponent_triangle

L1561 ↗
AlgebraicGeometry.Scheme.Etale.unitComponent_triangle
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
lemma unitComponent_triangle
    (X : (Spec (.of k)).Etale) :
    (geometricFiber k K).map (unitComponent k K X).hom ≫
        (geometricFiberCounitComponent k K
          ((geometricFiber k K).obj X)).hom =
      𝟙 ((geometricFiber k K).obj X)
def

unitIso

L1573 ↗
AlgebraicGeometry.Scheme.Etale.unitIso
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def unitIso :
    𝟭 ((Spec (.of k)).Etale) ≅
      geometricFiber k K ⋙ inverseFunctor k K
def

assembledEquivalence

L1624 ↗
AlgebraicGeometry.Scheme.Etale.assembledEquivalence
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · full declaration
def assembledEquivalence :
    (Spec (.of k)).Etale ≌
      DiscreteContAction TopCat (K ≃ₐ[k] K) where
  functor := geometricFiber k K
  inverse := inverseFunctor k K
  unitIso := unitIso k K
  counitIso := inverseCounitIso k K
  functor_unitIso_comp X := unitComponent_triangle k K X
opaque

equivDiscreteContAction

L1638 ↗
AlgebraicGeometry.Scheme.Etale.equivDiscreteContAction
Documentation

Stacks Project, Tag 03QR. Étale schemes over a field are equivalent to discrete continuous sets with an action of its absolute Galois group. The forward functor is the geometric fiber at Spec K.

Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
opaque equivDiscreteContAction :
    (Spec (.of k)).Etale ≌
      DiscreteContAction TopCat (K ≃ₐ[k] K)
instance

geometricFiberIsEquivalence

L1643 ↗
AlgebraicGeometry.Scheme.Etale.geometricFiberIsEquivalence
Source context 8 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits MorphismProperty PreGaloisCategory
open scoped AlgebraicGeometry.FiniteEtale FintypeCatDiscrete
namespace AlgebraicGeometry.Scheme.Etale
variable (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
instance geometricFiberIsEquivalence :
    (geometricFiber k K).IsEquivalence

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