Étale cohomology foundations

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

DefinitionTauCeti.Compactification.commonRefinement#

The common refinement of two compactifications: the scheme-theoretic closure of the source in the fibre product of their ambient schemes over the base.

TauCeti.Compactification.commonRefinement.{u} {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S}
  (C₁ C₂ : TauCeti.Compactification f) : TauCeti.DenseCompactification f
Lean

Formalized in Tau Ceti as TauCeti.Compactification.commonRefinement.

Sources
LeanTauCeti.Compactification.commonRefinement
Uses 2 · Used by 2
Statement usesTauCeti.Compactification · TauCeti.DenseCompactification
Used byTauCeti.Compactification.exists_forall_nonempty_hom · TauCeti.DenseCompactification.isLimitCommonRefinementFan

DefinitionTauCeti.DenseCompactification.isLimitCommonRefinementFan#

The common refinement is the binary product in the category of dense compactifications.

TauCeti.DenseCompactification.isLimitCommonRefinementFan.{u} {X S : AlgebraicGeometry.Scheme}
  {f : X ⟶ S} (D₁ D₂ : TauCeti.DenseCompactification f) :
  CategoryTheory.Limits.IsLimit (D₁.commonRefinementFan D₂)
Lean

Formalized in Tau Ceti as TauCeti.DenseCompactification.isLimitCommonRefinementFan.

Sources
LeanTauCeti.DenseCompactification.isLimitCommonRefinementFan
Uses 3
Statement usesTauCeti.Compactification · TauCeti.Compactification.commonRefinement · TauCeti.DenseCompactification

TheoremTauCeti.Compactification.exists_forall_nonempty_hom#

Every nonempty finite family of compactifications has a dense common refinement.

TauCeti.Compactification.exists_forall_nonempty_hom.{u, u_1} {X S : AlgebraicGeometry.Scheme}
  {f : X ⟶ S} {ι : Type u_1} [Finite ι] [Nonempty ι] (C : ι → TauCeti.Compactification f) :
  ∃ E, ∀ (i : ι), Nonempty (E.obj ⟶ C i)
Lean

Formalized in Tau Ceti as TauCeti.Compactification.exists_forall_nonempty_hom.

Sources
LeanTauCeti.Compactification.exists_forall_nonempty_hom
Uses 3
Statement usesTauCeti.Compactification · TauCeti.DenseCompactification
Proof usesTauCeti.Compactification.commonRefinement

TheoremTauCeti.Compactification.hom_unique#

Maps from a compactification with schematically dense interior to any fixed compactification are unique. No density assumption on the target is needed.

TauCeti.Compactification.hom_unique.{u} {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S}
  {C D : TauCeti.Compactification f} [AlgebraicGeometry.IsSchemeTheoreticallyDominant C.j]
  (h k : C ⟶ D) : h = k
Lean

Formalized in Tau Ceti as TauCeti.Compactification.hom_unique.

Sources
LeanTauCeti.Compactification.hom_unique
Uses 1
Statement usesTauCeti.Compactification

TheoremTauCeti.FiniteEtaleScheme.exists_isColimit_binaryCofanMk_of_mono#

Every monomorphism i : X ⟶ Y of finite étale schemes over S is the inclusion of a direct summand: there is a finite étale Z over S with a morphism u : Z ⟶ Y exhibiting Y as the coproduct of X and Z. Here Z is the open complement of the image of i.

TauCeti.FiniteEtaleScheme.exists_isColimit_binaryCofanMk_of_mono.{u} {S : AlgebraicGeometry.Scheme}
  {X Y : TauCeti.FiniteEtaleScheme S} (i : X ⟶ Y) [CategoryTheory.Mono i] :
  ∃ Z u, Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk i u))
Lean

Formalized in Tau Ceti as TauCeti.FiniteEtaleScheme.exists_isColimit_binaryCofanMk_of_mono.

Sources
LeanTauCeti.FiniteEtaleScheme.exists_isColimit_binaryCofanMk_of_mono
Used by 1
Used byTauCeti.FiniteEtaleScheme.epi_iff_surjective

TheoremTauCeti.FiniteEtaleScheme.epi_iff_surjective#

A morphism of finite étale schemes is an epimorphism if and only if its underlying morphism of schemes is surjective.

TauCeti.FiniteEtaleScheme.epi_iff_surjective.{u} {S : AlgebraicGeometry.Scheme}
  {X Y : TauCeti.FiniteEtaleScheme S} (g : X ⟶ Y) :
  CategoryTheory.Epi g ↔ AlgebraicGeometry.Surjective (CategoryTheory.Over.Hom.left g.hom)
Lean

Formalized in Tau Ceti as TauCeti.FiniteEtaleScheme.epi_iff_surjective.

Sources
LeanTauCeti.FiniteEtaleScheme.epi_iff_surjective
Uses 1
Proof usesTauCeti.FiniteEtaleScheme.exists_isColimit_binaryCofanMk_of_mono

TheoremThe invariants of a finite étale algebra under a finite monoid of algebra endomorphisms form an étale algebra# 

TauCeti.FixedPoints.etale_subalgebra.{u, u_1} {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
  (G : Type u_1) [Monoid G] [MulSemiringAction G S] [SMulCommClass G R S] [Algebra.Etale R S]
  [Module.Finite R S] [Finite G] : Algebra.Etale R ↥(FixedPoints.subalgebra R S G)
Lean

Formalized in Tau Ceti as TauCeti.FixedPoints.etale_subalgebra.

Sources
LeanTauCeti.FixedPoints.etale_subalgebra

AbbreviationTauCeti.Compactification#

Compactifications of f, with maps fixing X and lying over S.

TauCeti.Compactification.{u} {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) : Type (u + 1)
Lean

Formalized in Tau Ceti as TauCeti.Compactification.

Sources
LeanTauCeti.Compactification
Used by 5
Used byTauCeti.Compactification.commonRefinement · TauCeti.Compactification.exists_forall_nonempty_hom · TauCeti.Compactification.hom_unique · TauCeti.DenseCompactification · TauCeti.DenseCompactification.isLimitCommonRefinementFan

AbbreviationTauCeti.DenseCompactification#

The full subcategory of compactifications with scheme-theoretically dense interior.

TauCeti.DenseCompactification.{u} {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) : Type (u + 1)
Lean

Formalized in Tau Ceti as TauCeti.DenseCompactification.

Sources
LeanTauCeti.DenseCompactification
Uses 1 · Used by 3
Statement usesTauCeti.Compactification
Used byTauCeti.Compactification.commonRefinement · TauCeti.Compactification.exists_forall_nonempty_hom · TauCeti.DenseCompactification.isLimitCommonRefinementFan

DefinitionTauCeti.FiniteEtaleScheme.fiber#

The geometric fibre functor at a geometric point x : Spec Ω ⟶ S, for Ω separably closed: a finite étale S-scheme X goes to the finite set classifying X ×_S Spec Ω.

TauCeti.FiniteEtaleScheme.fiber.{u} {S : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω]
  [IsSepClosed Ω] (x : AlgebraicGeometry.Spec ↧Ω ⟶ S) :
  CategoryTheory.Functor (TauCeti.FiniteEtaleScheme S) FintypeCat
Lean

Formalized in Tau Ceti as TauCeti.FiniteEtaleScheme.fiber.

Sources
LeanTauCeti.FiniteEtaleScheme.fiber

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.