Category of finite étale R-algebras

In this file we define the category of finite étale R-algebras over a ring R. For any geometric point Ω of R, we define a fiber functor sending a finite étale R-algebra S to the finite set of R-algebra homomorphisms S →ₐ[R] Ω.

Main definitions

• CommAlgCat.FiniteEtale: The category of finite étale R-algebras.
• CommAlgCat.FiniteEtale.fiber: For a geometric point Ω of R, the fiber functor S ↦ (S →ₐ[R] Ω).

Main results

• CommAlgCat.FiniteEtale.equivOfIsSepClosed: If R = Ω is separably closed, the category of finite étale Ω-algebras is anti-equivalent to FintypeCat. In particular, the functor CommAlgCat.FiniteEtale.fiber is an equivalence of categories in this case.

@[reducible, inline]

abbrev CommAlgCat.finite (R : Type u) [CommRing R] : CategoryTheory.ObjectProperty (CommAlgCat R)

The object property of finite R-algebras.

Equations

• CommAlgCat.finite R S = Module.Finite R ↑S

@[reducible, inline]

abbrev CommAlgCat.etale (R : Type u) [CommRing R] : CategoryTheory.ObjectProperty (CommAlgCat R)

The object property of étale R-algebras.

Equations

• CommAlgCat.etale R S = Algebra.Etale R ↑S

@[reducible, inline]

abbrev CommAlgCat.finiteEtale (R : Type u) [CommRing R] : CategoryTheory.ObjectProperty (CommAlgCat R)

The object property of finite étale R-algebras.

Equations

• CommAlgCat.finiteEtale R = CommAlgCat.finite R ⊓ CommAlgCat.etale R

@[reducible, inline]

abbrev CommAlgCat.FiniteEtale (R : Type u) [CommRing R] : Type (max u (v + 1))

The category of finite étale R-algebras.

Equations

• CommAlgCat.FiniteEtale R = (CommAlgCat.finiteEtale R).FullSubcategory

@[implicit_reducible]

instance CommAlgCat.instCoeSortFiniteEtaleType (R : Type u) [CommRing R] : CoeSort (FiniteEtale R) (Type v)

Equations

• CommAlgCat.instCoeSortFiniteEtaleType R = { coe := fun (R_1 : CommAlgCat.FiniteEtale R) => ↑R_1.obj }

instance CommAlgCat.instEtaleCarrierObjFiniteEtale (R : Type u) [CommRing R] (S : FiniteEtale R) : Algebra.Etale R ↑S.obj

instance CommAlgCat.instFiniteCarrierObjFiniteEtale (R : Type u) [CommRing R] (S : FiniteEtale R) : Module.Finite R ↑S.obj

@[reducible, inline]

abbrev CommAlgCat.FiniteEtale.of (R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S] [Module.Finite R S] [Algebra.Etale R S] : FiniteEtale R

Construct a term of FiniteEtale R from a finite étale R-algebra.

Equations

• CommAlgCat.FiniteEtale.of R S = { obj := CommAlgCat.of R S, property := ⋯ }

@[simp]

theorem CommAlgCat.FiniteEtale.of_obj (R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S] [Module.Finite R S] [Algebra.Etale R S] : (of R S).obj = CommAlgCat.of R S

@[reducible, inline]

abbrev CommAlgCat.FiniteEtale.ofHom {R : Type u} [CommRing R] {S T : Type v} [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Module.Finite R S] [Algebra.Etale R S] [Module.Finite R T] [Algebra.Etale R T] (f : S →ₐ[R] T) : of R S ⟶ of R T

Construct a morphism in FiniteEtale R from an algebra map.

Equations

• CommAlgCat.FiniteEtale.ofHom f = { hom := CommAlgCat.ofHom f }

@[simp]

theorem CommAlgCat.FiniteEtale.ofHom_hom {R : Type u} [CommRing R] {S T : Type v} [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Module.Finite R S] [Algebra.Etale R S] [Module.Finite R T] [Algebra.Etale R T] (f : S →ₐ[R] T) : (ofHom f).hom = CommAlgCat.ofHom f

@[reducible, inline]

abbrev CommAlgCat.FiniteEtale.isoMk {R : Type u} [CommRing R] {S T : FiniteEtale R} (e : ↑S.obj ≃ₐ[R] ↑T.obj) : S ≅ T

Construct an isomorphism in FiniteEtale R from an algebra equivalence.

Equations

• CommAlgCat.FiniteEtale.isoMk e = (CommAlgCat.finiteEtale R).isoMk (CommAlgCat.isoMk e)

instance CommAlgCat.instIsArtinianRingCarrierObjFiniteEtale (k : Type u) [Field k] (R : FiniteEtale k) : IsArtinianRing ↑R.obj

def CommAlgCat.FiniteEtale.baseChange (R : Type u) [CommRing R] (S : Type w) [CommRing S] [Algebra R S] : CategoryTheory.Functor (FiniteEtale R) (FiniteEtale S)

If S is an R-algebra, this is the base change functor A ↦ S ⊗[R] A.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommAlgCat.FiniteEtale.baseChange_obj_obj_carrier (R : Type u) [CommRing R] (S : Type w) [CommRing S] [Algebra R S] (A : FiniteEtale R) : ↑((baseChange R S).obj A).obj = TensorProduct R S ↑A.obj

@[simp]

theorem CommAlgCat.FiniteEtale.baseChange_map_hom (R : Type u) [CommRing R] (S : Type w) [CommRing S] [Algebra R S] {A B : FiniteEtale R} (f : A ⟶ B) : ((baseChange R S).map f).hom = CommAlgCat.ofHom (Algebra.TensorProduct.map (AlgHom.id S S) (Hom.hom f.hom))

def CommAlgCat.FiniteEtale.baseChangeSelfIso (R : Type u) [CommRing R] : baseChange R R ≅ CategoryTheory.Functor.id (FiniteEtale R)

Base change from R to R is isomorphic to the identity.

Equations

• CommAlgCat.FiniteEtale.baseChangeSelfIso R = CategoryTheory.NatIso.ofComponents (fun (A : CommAlgCat.FiniteEtale R) => CommAlgCat.FiniteEtale.isoMk (Algebra.TensorProduct.lid R ↑A.obj)) ⋯

def CommAlgCat.FiniteEtale.fiber (R : Type u) [CommRing R] (Ω : Type w) [Field Ω] [Algebra R Ω] : CategoryTheory.Functor (FiniteEtale R)ᵒᵖ FintypeCat

The fiber functor for finite étale R-algebras at the geometric point Ω: This is the functor sending S to R-algebra homomorphisms S →ₐ[R] Ω.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommAlgCat.FiniteEtale.fiber_map (R : Type u) [CommRing R] (Ω : Type w) [Field Ω] [Algebra R Ω] {S T : (FiniteEtale R)ᵒᵖ} (f : S ⟶ T) : (fiber R Ω).map f = FintypeCat.homMk fun (x : (FintypeCat.of (↑(Opposite.unop S).obj →ₐ[R] Ω)).obj) => AlgHom.comp x (Hom.hom f.unop.hom)

@[simp]

theorem CommAlgCat.FiniteEtale.fiber_obj_obj (R : Type u) [CommRing R] (Ω : Type w) [Field Ω] [Algebra R Ω] (S : (FiniteEtale R)ᵒᵖ) : ((fiber R Ω).obj S).obj = (↑(Opposite.unop S).obj →ₐ[R] Ω)

def CommAlgCat.FiniteEtale.finiteSpec (k : Type u) [Field k] : CategoryTheory.Functor (FiniteEtale k)ᵒᵖ FintypeCat

If k is a field, this is the Spec functor sending a finite étale k-algebra R to its finite prime spectrum.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommAlgCat.FiniteEtale.finiteSpec_map (k : Type u) [Field k] {X✝ Y✝ : (FiniteEtale k)ᵒᵖ} (f : X✝ ⟶ Y✝) : (finiteSpec k).map f = FintypeCat.homMk (PrimeSpectrum.comap ↑(Hom.hom f.unop.hom))

@[simp]

theorem CommAlgCat.FiniteEtale.finiteSpec_obj_obj (k : Type u) [Field k] (R : (FiniteEtale k)ᵒᵖ) : ((finiteSpec k).obj R).obj = PrimeSpectrum ↑(Opposite.unop R).obj

def CommAlgCat.FiniteEtale.fiberIsoBaseChangeFiber (R : Type u) [CommRing R] (Ω : Type w) [Field Ω] [Algebra R Ω] (S : Type w) [CommRing S] [Algebra R S] [Algebra S Ω] [IsScalarTower R S Ω] : fiber R Ω ≅ (baseChange R S).op.comp (fiber S Ω)

If the geometric point Ω factors through S, the fiber can be computed after base change to S.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommAlgCat.FiniteEtale.fiberIsoFiniteSpec (Ω : Type w) [Field Ω] [IsSepClosed Ω] : fiber Ω Ω ≅ finiteSpec Ω

If Ω is separably closed, the fiber functor for finite étale Ω-algebras is naturally isomorphic to the (finite) Spec functor.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommAlgCat.FiniteEtale.fiberIsoComp (R : Type u) [CommRing R] (Ω : Type w) [Field Ω] [Algebra R Ω] [IsSepClosed Ω] : fiber R Ω ≅ (baseChange R Ω).op.comp (finiteSpec Ω)

If Ω is separably closed, the fiber S →ₐ[R] Ω is isomorphic to the prime spectrum of the base change Ω ⊗[R] S.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommAlgCat.FiniteEtale.equivOfIsSepClosed (Ω : Type u) [Field Ω] [IsSepClosed Ω] : (FiniteEtale Ω)ᵒᵖ ≌ FintypeCat

If Ω is a separably closed field, the category of finite étale Ω-algebras is anti-equivalent to FintypeCat.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommAlgCat.FiniteEtale.equivOfIsSepClosed_functor (Ω : Type u) [Field Ω] [IsSepClosed Ω] : (equivOfIsSepClosed Ω).functor = finiteSpec Ω

@[simp]

theorem CommAlgCat.FiniteEtale.equivOfIsSepClosed_inverse_map (Ω : Type u) [Field Ω] [IsSepClosed Ω] {X Y : FintypeCat} (f : X ⟶ Y) : (equivOfIsSepClosed Ω).inverse.map f = (ofHom (AlgHom.pi fun (i : X.obj) => Pi.evalAlgHom Ω (fun (a : Y.obj) => Ω) ((CategoryTheory.ConcreteCategory.hom f) i))).op

@[simp]

theorem CommAlgCat.FiniteEtale.equivOfIsSepClosed_inverse_obj (Ω : Type u) [Field Ω] [IsSepClosed Ω] (X : FintypeCat) : (equivOfIsSepClosed Ω).inverse.obj X = Opposite.op (of Ω (X.obj → Ω))

instance CommAlgCat.instIsEquivalenceOppositeFiniteEtaleFintypeCatFiniteSpecOfIsSepClosed (Ω : Type u) [Field Ω] [IsSepClosed Ω] : (FiniteEtale.finiteSpec Ω).IsEquivalence

instance CommAlgCat.instIsEquivalenceOppositeFiniteEtaleFintypeCatFiberOfIsSepClosed (Ω : Type u) [Field Ω] [IsSepClosed Ω] : (FiniteEtale.fiber Ω Ω).IsEquivalence