ModuleRecoveredCoefficientRecovery.lean
Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.RecoveredCoefficientRecovery
2 declarations indexed from sourceView source ↗ Module documentation
Recovered Coefficient Recovery
The recovered literal coefficient charts form an actual cover of the input scheme.
Declarations
EtaleFundamentalGroups.recoveredCoefficientChartCover
DocumentationThe recovered literal coefficient charts form an actual cover of the input scheme.
Source context 13 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))
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 "φ" => 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))
local notation "D" => Scheme.Cover.recoveredOverlapGlueData 𝒰L Z ML e
EtaleFundamentalGroups.recoveredCoefficientTransition_isPullback
DocumentationThe literal coefficient overlap is the actual intersection of the two recovered literal charts in the input scheme.
Source context 13 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))
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 "φ" => 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))
local notation "D" => Scheme.Cover.recoveredOverlapGlueData 𝒰L Z ML e