NYLL
Module

RecoveredCoefficientTransitions.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.RecoveredCoefficientTransitions
10 declarations indexed from sourceView source ↗

Module documentation

Coefficient transitions for recovered local models

Recovered overlap maps are transported to literal coefficient extensions. Their transitions preserve the coefficient projections and recover the original chart maps.

Imports4
Imported by3

Declarations

def

recoveredCoefficientOverlapIso

L41 ↗
EtaleFundamentalGroups.recoveredCoefficientOverlapIso
Documentation

Identify a literal coefficient-extended overlap with the recovered gluing overlap.

Source context 15 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (S : Scheme.{u}) (f : S ⟶ Spec (CommRingCat.of k)) (𝒰 : S.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
local notation "φ" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "𝒰L" => constantFieldOpenCover k L S f 𝒰
local notation "ML" => (fun i : 𝒰.I₀ ↦
  Functor.obj (Over.pullback (pullback.snd φ (𝒰.f i ≫ f))) (M i))
variable (Z : Over (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L)))
    (𝒰.f i ≫ f))).obj (M i) ≅
      (Over.pullback ((constantFieldOpenCover k L S f 𝒰).f i)).obj Z)
local notation "D" => Scheme.Cover.recoveredOverlapGlueData 𝒰L Z ML e
local notation "a" => (fun i : 𝒰.I₀ ↦ Comma.hom (M i) ≫ 𝒰.f i)
local notation "v" => (fun i j : 𝒰.I₀ ↦ pullback.fst (a i) (𝒰.f j) ≫ a i)
Lean source · statement
def recoveredCoefficientOverlapIso (i j : 𝒰.I₀) :
    pullback φ (v i j ≫ f) ≅ (D).V (i, j)
theorem

recoveredCoefficientOverlapIso_base

L45 ↗
EtaleFundamentalGroups.recoveredCoefficientOverlapIso_base
Source context 15 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (S : Scheme.{u}) (f : S ⟶ Spec (CommRingCat.of k)) (𝒰 : S.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
local notation "φ" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "𝒰L" => constantFieldOpenCover k L S f 𝒰
local notation "ML" => (fun i : 𝒰.I₀ ↦
  Functor.obj (Over.pullback (pullback.snd φ (𝒰.f i ≫ f))) (M i))
variable (Z : Over (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L)))
    (𝒰.f i ≫ f))).obj (M i) ≅
      (Over.pullback ((constantFieldOpenCover k L S f 𝒰).f i)).obj Z)
local notation "D" => Scheme.Cover.recoveredOverlapGlueData 𝒰L Z ML e
local notation "a" => (fun i : 𝒰.I₀ ↦ Comma.hom (M i) ≫ 𝒰.f i)
local notation "v" => (fun i j : 𝒰.I₀ ↦ pullback.fst (a i) (𝒰.f j) ≫ a i)
Lean source · statement
theorem recoveredCoefficientOverlapIso_base (i j : 𝒰.I₀) :
    (recoveredCoefficientOverlapIso k L S f 𝒰 M Z e i j).hom ≫
        (D).f i j ≫ (ML i).hom ≫ (𝒰L).f i = coefficientModelMap φ f (v i j)
def

recoveredCoefficientTransition

L51 ↗
EtaleFundamentalGroups.recoveredCoefficientTransition
Documentation

Transport the recovered transition to the literal coefficient-extended overlaps.

Source context 15 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (S : Scheme.{u}) (f : S ⟶ Spec (CommRingCat.of k)) (𝒰 : S.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
local notation "φ" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "𝒰L" => constantFieldOpenCover k L S f 𝒰
local notation "ML" => (fun i : 𝒰.I₀ ↦
  Functor.obj (Over.pullback (pullback.snd φ (𝒰.f i ≫ f))) (M i))
variable (Z : Over (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L)))
    (𝒰.f i ≫ f))).obj (M i) ≅
      (Over.pullback ((constantFieldOpenCover k L S f 𝒰).f i)).obj Z)
local notation "D" => Scheme.Cover.recoveredOverlapGlueData 𝒰L Z ML e
local notation "a" => (fun i : 𝒰.I₀ ↦ Comma.hom (M i) ≫ 𝒰.f i)
local notation "v" => (fun i j : 𝒰.I₀ ↦ pullback.fst (a i) (𝒰.f j) ≫ a i)
Lean source · statement
def recoveredCoefficientTransition (i j : 𝒰.I₀) :
    pullback φ (v i j ≫ f) ⟶ pullback φ (v j i ≫ f)
theorem

recoveredCoefficientTransition_base

L56 ↗
EtaleFundamentalGroups.recoveredCoefficientTransition_base
Source context 15 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (S : Scheme.{u}) (f : S ⟶ Spec (CommRingCat.of k)) (𝒰 : S.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
local notation "φ" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "𝒰L" => constantFieldOpenCover k L S f 𝒰
local notation "ML" => (fun i : 𝒰.I₀ ↦
  Functor.obj (Over.pullback (pullback.snd φ (𝒰.f i ≫ f))) (M i))
variable (Z : Over (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L)))
    (𝒰.f i ≫ f))).obj (M i) ≅
      (Over.pullback ((constantFieldOpenCover k L S f 𝒰).f i)).obj Z)
local notation "D" => Scheme.Cover.recoveredOverlapGlueData 𝒰L Z ML e
local notation "a" => (fun i : 𝒰.I₀ ↦ Comma.hom (M i) ≫ 𝒰.f i)
local notation "v" => (fun i j : 𝒰.I₀ ↦ pullback.fst (a i) (𝒰.f j) ≫ a i)
Lean source · statement
theorem recoveredCoefficientTransition_base (i j : 𝒰.I₀) :
    recoveredCoefficientTransition k L S f 𝒰 M Z e i j ≫
        coefficientModelMap φ f (v j i) = coefficientModelMap φ f (v i j)
theorem

recoveredCoefficientTransition_coefficient

L68 ↗
EtaleFundamentalGroups.recoveredCoefficientTransition_coefficient
Source context 15 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (S : Scheme.{u}) (f : S ⟶ Spec (CommRingCat.of k)) (𝒰 : S.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
local notation "φ" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "𝒰L" => constantFieldOpenCover k L S f 𝒰
local notation "ML" => (fun i : 𝒰.I₀ ↦
  Functor.obj (Over.pullback (pullback.snd φ (𝒰.f i ≫ f))) (M i))
variable (Z : Over (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L)))
    (𝒰.f i ≫ f))).obj (M i) ≅
      (Over.pullback ((constantFieldOpenCover k L S f 𝒰).f i)).obj Z)
local notation "D" => Scheme.Cover.recoveredOverlapGlueData 𝒰L Z ML e
local notation "a" => (fun i : 𝒰.I₀ ↦ Comma.hom (M i) ≫ 𝒰.f i)
local notation "v" => (fun i j : 𝒰.I₀ ↦ pullback.fst (a i) (𝒰.f j) ≫ a i)
Lean source · statement
theorem recoveredCoefficientTransition_coefficient (i j : 𝒰.I₀) :
    recoveredCoefficientTransition k L S f 𝒰 M Z e i j ≫
        pullback.fst φ (v j i ≫ f) = pullback.fst φ (v i j ≫ f)
theorem

recoveredCoefficientTransition_original

L75 ↗
EtaleFundamentalGroups.recoveredCoefficientTransition_original
Source context 15 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (S : Scheme.{u}) (f : S ⟶ Spec (CommRingCat.of k)) (𝒰 : S.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
local notation "φ" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "𝒰L" => constantFieldOpenCover k L S f 𝒰
local notation "ML" => (fun i : 𝒰.I₀ ↦
  Functor.obj (Over.pullback (pullback.snd φ (𝒰.f i ≫ f))) (M i))
variable (Z : Over (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L)))
    (𝒰.f i ≫ f))).obj (M i) ≅
      (Over.pullback ((constantFieldOpenCover k L S f 𝒰).f i)).obj Z)
local notation "D" => Scheme.Cover.recoveredOverlapGlueData 𝒰L Z ML e
local notation "a" => (fun i : 𝒰.I₀ ↦ Comma.hom (M i) ≫ 𝒰.f i)
local notation "v" => (fun i j : 𝒰.I₀ ↦ pullback.fst (a i) (𝒰.f j) ≫ a i)
Lean source · statement
theorem recoveredCoefficientTransition_original (i j : 𝒰.I₀) :
    recoveredCoefficientTransition k L S f 𝒰 M Z e i j ≫
        pullback.snd φ (v j i ≫ f) ≫ v j i = pullback.snd φ (v i j ≫ f) ≫ v i j
def

recoveredCoefficientChartMap

L83 ↗
EtaleFundamentalGroups.recoveredCoefficientChartMap
Documentation

The original recovered chart map expressed on the literal coefficient extension.

Source context 15 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (S : Scheme.{u}) (f : S ⟶ Spec (CommRingCat.of k)) (𝒰 : S.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
local notation "φ" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "𝒰L" => constantFieldOpenCover k L S f 𝒰
local notation "ML" => (fun i : 𝒰.I₀ ↦
  Functor.obj (Over.pullback (pullback.snd φ (𝒰.f i ≫ f))) (M i))
variable (Z : Over (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L)))
    (𝒰.f i ≫ f))).obj (M i) ≅
      (Over.pullback ((constantFieldOpenCover k L S f 𝒰).f i)).obj Z)
local notation "D" => Scheme.Cover.recoveredOverlapGlueData 𝒰L Z ML e
local notation "a" => (fun i : 𝒰.I₀ ↦ Comma.hom (M i) ≫ 𝒰.f i)
local notation "v" => (fun i j : 𝒰.I₀ ↦ pullback.fst (a i) (𝒰.f j) ≫ a i)
Lean source · statement
def recoveredCoefficientChartMap (i : 𝒰.I₀) :
    pullback φ (a i ≫ f) ⟶ Z.left
theorem

recoveredCoefficientChartMap_isOpenImmersion

L88 ↗
EtaleFundamentalGroups.recoveredCoefficientChartMap_isOpenImmersion
Source context 15 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (S : Scheme.{u}) (f : S ⟶ Spec (CommRingCat.of k)) (𝒰 : S.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
local notation "φ" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "𝒰L" => constantFieldOpenCover k L S f 𝒰
local notation "ML" => (fun i : 𝒰.I₀ ↦
  Functor.obj (Over.pullback (pullback.snd φ (𝒰.f i ≫ f))) (M i))
variable (Z : Over (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L)))
    (𝒰.f i ≫ f))).obj (M i) ≅
      (Over.pullback ((constantFieldOpenCover k L S f 𝒰).f i)).obj Z)
local notation "D" => Scheme.Cover.recoveredOverlapGlueData 𝒰L Z ML e
local notation "a" => (fun i : 𝒰.I₀ ↦ Comma.hom (M i) ≫ 𝒰.f i)
local notation "v" => (fun i j : 𝒰.I₀ ↦ pullback.fst (a i) (𝒰.f j) ≫ a i)
Lean source · statement
theorem recoveredCoefficientChartMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredCoefficientChartMap k L S f 𝒰 M Z e i)
theorem

recoveredCoefficientOverlapIso_chartMap

L97 ↗
EtaleFundamentalGroups.recoveredCoefficientOverlapIso_chartMap
Source context 15 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (S : Scheme.{u}) (f : S ⟶ Spec (CommRingCat.of k)) (𝒰 : S.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
local notation "φ" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "𝒰L" => constantFieldOpenCover k L S f 𝒰
local notation "ML" => (fun i : 𝒰.I₀ ↦
  Functor.obj (Over.pullback (pullback.snd φ (𝒰.f i ≫ f))) (M i))
variable (Z : Over (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L)))
    (𝒰.f i ≫ f))).obj (M i) ≅
      (Over.pullback ((constantFieldOpenCover k L S f 𝒰).f i)).obj Z)
local notation "D" => Scheme.Cover.recoveredOverlapGlueData 𝒰L Z ML e
local notation "a" => (fun i : 𝒰.I₀ ↦ Comma.hom (M i) ≫ 𝒰.f i)
local notation "v" => (fun i j : 𝒰.I₀ ↦ pullback.fst (a i) (𝒰.f j) ≫ a i)
Lean source · statement
theorem recoveredCoefficientOverlapIso_chartMap (i j : 𝒰.I₀) :
    (recoveredCoefficientOverlapIso k L S f 𝒰 M Z e i j).hom ≫
        (D).f i j ≫ Scheme.Cover.recoveredLocalModelMap 𝒰L Z ML e i =
      coefficientOverlapFirstMap φ f (𝒰.f i) (𝒰.f j) (M i).hom ≫
        recoveredCoefficientChartMap k L S f 𝒰 M Z e i
theorem

recoveredCoefficientTransition_chartMap

L110 ↗
EtaleFundamentalGroups.recoveredCoefficientTransition_chartMap
Documentation

The literal coefficient transitions recover the same map to the original cover.

Source context 15 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (S : Scheme.{u}) (f : S ⟶ Spec (CommRingCat.of k)) (𝒰 : S.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
local notation "φ" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "𝒰L" => constantFieldOpenCover k L S f 𝒰
local notation "ML" => (fun i : 𝒰.I₀ ↦
  Functor.obj (Over.pullback (pullback.snd φ (𝒰.f i ≫ f))) (M i))
variable (Z : Over (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L)))
    (𝒰.f i ≫ f))).obj (M i) ≅
      (Over.pullback ((constantFieldOpenCover k L S f 𝒰).f i)).obj Z)
local notation "D" => Scheme.Cover.recoveredOverlapGlueData 𝒰L Z ML e
local notation "a" => (fun i : 𝒰.I₀ ↦ Comma.hom (M i) ≫ 𝒰.f i)
local notation "v" => (fun i j : 𝒰.I₀ ↦ pullback.fst (a i) (𝒰.f j) ≫ a i)
Lean source · statement
theorem recoveredCoefficientTransition_chartMap (i j : 𝒰.I₀) :
    recoveredCoefficientTransition k L S f 𝒰 M Z e i j ≫
        coefficientOverlapFirstMap φ f (𝒰.f j) (𝒰.f i) (M j).hom ≫
          recoveredCoefficientChartMap k L S f 𝒰 M Z e j =
      coefficientOverlapFirstMap φ f (𝒰.f i) (𝒰.f j) (M i).hom ≫
        recoveredCoefficientChartMap k L S f 𝒰 M Z e i

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