NYLL
Module

RawOverlapSupplier.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.RawOverlapSupplier
11 declarations indexed from sourceView source ↗

Module documentation

Raw Overlap Supplier

The literal coefficient extension of a local model, over its coefficient base.

Imports3
Imported by2

Declarations

abbrev

coefficientLocalModelOver

L24 ↗
EtaleFundamentalGroups.coefficientLocalModelOver
Documentation

The literal coefficient extension of a local model, over its coefficient base.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
abbrev coefficientLocalModelOver : Over T'
abbrev

coefficientOverlapOver

L28 ↗
EtaleFundamentalGroups.coefficientOverlapOver
Documentation

The literal coefficient extension of an overlap, over its coefficient base.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
abbrev coefficientOverlapOver : Over T'
def

coefficientOverlapInclusion

L32 ↗
EtaleFundamentalGroups.coefficientOverlapInclusion
Documentation

The literal coefficient extension of the first overlap inclusion.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
def coefficientOverlapInclusion :
    coefficientOverlapOver φ f u v y ⟶ coefficientLocalModelOver φ f u y
def

coefficientLocalModelStructure

L37 ↗
EtaleFundamentalGroups.coefficientLocalModelStructure
Documentation

The actual local-model map to the coefficient-extended base chart.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
def coefficientLocalModelStructure :
    (coefficientLocalModelOver φ f u y).left ⟶ pullback φ (u ≫ f)
def

coefficientOverlapSecondMap

L42 ↗
EtaleFundamentalGroups.coefficientOverlapSecondMap
Documentation

The actual second map of the coefficient-extended overlap.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
def coefficientOverlapSecondMap :
    (coefficientOverlapOver φ f u v y).left ⟶ pullback φ (v ≫ f)
theorem

coefficientOverlap_isPullback

L47 ↗
EtaleFundamentalGroups.coefficientOverlap_isPullback
Documentation

The raw coefficient-extended overlap is cartesian over the extended cover.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
theorem coefficientOverlap_isPullback :
    IsPullback (coefficientOverlapInclusion φ f u v y).left
      (coefficientOverlapSecondMap φ f u v y)
      (coefficientLocalModelStructure φ f u y ≫ coefficientModelMap φ f u)
      (coefficientModelMap φ f v)
theorem

coefficientLocalModelStructure_isPullback

L68 ↗
EtaleFundamentalGroups.coefficientLocalModelStructure_isPullback
Documentation

The local model structure is the actual base change of the original one.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
theorem coefficientLocalModelStructure_isPullback :
    IsPullback (coefficientLocalModelStructure φ f u y)
      (pullback.snd φ ((y ≫ u) ≫ f))
      (pullback.snd φ (u ≫ f)) y
theorem

coefficientLocalModelStructure_finiteEtale

L82 ↗
EtaleFundamentalGroups.coefficientLocalModelStructure_finiteEtale
Documentation

Actual finite étale local models remain finite étale on the literal extension.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
theorem coefficientLocalModelStructure_finiteEtale [IsFiniteEtale y] :
    IsFiniteEtale (coefficientLocalModelStructure φ f u y)
theorem

coefficientLocalModelStructure_base

L89 ↗
EtaleFundamentalGroups.coefficientLocalModelStructure_base
Documentation

The local structure and chart inclusion agree with the literal total-model map.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
theorem coefficientLocalModelStructure_base :
    coefficientLocalModelStructure φ f u y ≫ coefficientModelMap φ f u =
      coefficientModelMap φ f (y ≫ u)
theorem

coefficientOverlapInclusion_base

L95 ↗
EtaleFundamentalGroups.coefficientOverlapInclusion_base
Documentation

The first overlap inclusion preserves the actual map to the extended base.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
theorem coefficientOverlapInclusion_base :
    (coefficientOverlapInclusion φ f u v y).left ≫
        coefficientLocalModelStructure φ f u y ≫ coefficientModelMap φ f u =
      coefficientModelMap φ f (pullback.fst (y ≫ u) v ≫ (y ≫ u))
theorem

coefficientOverlapFirstMap_stage_naturality

L116 ↗
EtaleFundamentalGroups.coefficientOverlapFirstMap_stage_naturality
Documentation

The actual coefficient cone maps preserve the first overlap inclusions.

Source context 13 commands

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

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
section FieldStage
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (S U V Y : Scheme.{u}) (f : S ⟶ Spec (CommRingCat.of k))
variable (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U) (s : Finset L)
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "φE" => Spec.map (CommRingCat.ofHom
  (algebraMap k (IntermediateField.adjoin k (s : Set L))))
local notation "p" => (pullback.fst (y ≫ u) v ≫ (y ≫ u))
Lean source · statement
theorem coefficientOverlapFirstMap_stage_naturality :
    (constantFieldInverseLimitCone k L (pullback (y ≫ u) v) (p ≫ f)).π.app (op s) ≫
        coefficientOverlapFirstMap φE f u v y =
      coefficientOverlapFirstMap φL f u v y ≫
        (constantFieldInverseLimitCone k L Y ((y ≫ u) ≫ f)).π.app (op s)

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