NYLL
Module

RawStageGlue.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.RawStageGlue
23 declarations indexed from sourceView source ↗

Module documentation

Gluing local models from recovered transitions

Imports4
Imported by3

Declarations

theorem

rawGluingInclusion_open

L28 ↗
EtaleFundamentalGroups.rawGluingInclusion_open
Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
include hV in
Lean source · statement
theorem rawGluingInclusion_open (i j : 𝒰.I₀) : IsOpenImmersion (d i j).left
theorem

rawGluingInclusion_mono

L32 ↗
EtaleFundamentalGroups.rawGluingInclusion_mono
Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
include hV in
Lean source · statement
theorem rawGluingInclusion_mono (i j : 𝒰.I₀) : Mono (d i j)
theorem

rawGluingInclusion_isIso

L38 ↗
EtaleFundamentalGroups.rawGluingInclusion_isIso
Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
include hV in
Lean source · statement
theorem rawGluingInclusion_isIso (i : 𝒰.I₀) : IsIso (d i i)
theorem

rawGluingTransition_structure

L50 ↗
EtaleFundamentalGroups.rawGluingTransition_structure
Documentation

Preservation of the base gives the other chart structure equation.

Source context 13 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
include hV in
Lean source · statement
theorem rawGluingTransition_structure
    (hS : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j ≫ 𝒰.f j =
      (d i j).left ≫ y i ≫ 𝒰.f i) (i j : 𝒰.I₀) :
    (t i j).left ≫ (d j i).left ≫ y j = ℓ i j
abbrev

rawGluingTriple

L58 ↗
EtaleFundamentalGroups.rawGluingTriple
Source context 12 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
Lean source · statement
abbrev rawGluingTriple (i j k : 𝒰.I₀) : Over B
def

rawGluingTripleToOverlap

L61 ↗
EtaleFundamentalGroups.rawGluingTripleToOverlap
Source context 12 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
Lean source · statement
def rawGluingTripleToOverlap (i j k : 𝒰.I₀) :
    rawGluingTriple 𝒰 A V d i j k ⟶ V (j, k)
def

rawGluingTripleTransition

L88 ↗
EtaleFundamentalGroups.rawGluingTripleTransition
Source context 12 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
Lean source · statement
def rawGluingTripleTransition (i j k : 𝒰.I₀) :
    rawGluingTriple 𝒰 A V d i j k ⟶ rawGluingTriple 𝒰 A V d j k i
theorem

rawGluingTripleTransition_fac

L97 ↗
EtaleFundamentalGroups.rawGluingTripleTransition_fac
Source context 12 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
Lean source · statement
theorem rawGluingTripleTransition_fac (i j k : 𝒰.I₀) :
    rawGluingTripleTransition 𝒰 A V d y ℓ hV t ht i j k ≫ pullback.snd _ _ =
      pullback.fst _ _ ≫ t i j
abbrev

gluingRecoveryFunctor

L105 ↗
EtaleFundamentalGroups.gluingRecoveryFunctor
Documentation

The actual coefficient pullback, followed by forgetting its structure map.

Source context 13 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable {B' Z : Scheme.{u}} (ψ : B' ⟶ B)
Lean source · statement
abbrev gluingRecoveryFunctor : Over B ⥤ Scheme.{u}
instance

gluingRecoveryFunctor_faithful

L108 ↗
EtaleFundamentalGroups.gluingRecoveryFunctor_faithful
Source context 13 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable {B' Z : Scheme.{u}} (ψ : B' ⟶ B)
Lean source · statement
instance gluingRecoveryFunctor_faithful [Flat ψ] [Surjective ψ] :
    (gluingRecoveryFunctor ψ).Faithful
theorem

rawGluingTransition_id

L124 ↗
EtaleFundamentalGroups.rawGluingTransition_id
Source context 19 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable {B' Z : Scheme.{u}} (ψ : B' ⟶ B)
local instance gluingRecoveryFunctor_faithful [Flat ψ] [Surjective ψ] :
    (gluingRecoveryFunctor ψ).Faithful := by
  let : ∀ (T : Scheme.{u}) (g : T ⟶ B), Epi (pullback.fst g ψ) :=
    fun T g => Flat.epi_of_flat_of_surjective (pullback.fst g ψ)
  infer_instance
variable (h : ∀ i : 𝒰.I₀, (gluingRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (gluingRecoveryFunctor ψ).map (t i j) ≫ (gluingRecoveryFunctor ψ).map (d j i) ≫ h j =
    (gluingRecoveryFunctor ψ).map (d i j) ≫ h i)
variable (hinj : ∀ (T : Over B) (i j : 𝒰.I₀),
  Function.Injective ((gluingRecoveryFunctor ψ).map (X := T) (Y := V (i, j))))
include hV hrec hinj in
Lean source · statement
theorem rawGluingTransition_id (i : 𝒰.I₀) : t i i = 𝟙 _
theorem

rawGluingTripleTransition_chartMap

L133 ↗
EtaleFundamentalGroups.rawGluingTripleTransition_chartMap
Source context 20 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable {B' Z : Scheme.{u}} (ψ : B' ⟶ B)
local instance gluingRecoveryFunctor_faithful [Flat ψ] [Surjective ψ] :
    (gluingRecoveryFunctor ψ).Faithful := by
  let : ∀ (T : Scheme.{u}) (g : T ⟶ B), Epi (pullback.fst g ψ) :=
    fun T g => Flat.epi_of_flat_of_surjective (pullback.fst g ψ)
  infer_instance
variable (h : ∀ i : 𝒰.I₀, (gluingRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (gluingRecoveryFunctor ψ).map (t i j) ≫ (gluingRecoveryFunctor ψ).map (d j i) ≫ h j =
    (gluingRecoveryFunctor ψ).map (d i j) ≫ h i)
variable (hinj : ∀ (T : Over B) (i j : 𝒰.I₀),
  Function.Injective ((gluingRecoveryFunctor ψ).map (X := T) (Y := V (i, j))))
omit [∀ i : 𝒰.I₀, Mono (h i)] in
include hrec in
Lean source · statement
theorem rawGluingTripleTransition_chartMap (i j k : 𝒰.I₀) :
    (gluingRecoveryFunctor ψ).map (rawGluingTripleTransition 𝒰 A V d y ℓ hV t ht i j k) ≫
      (gluingRecoveryFunctor ψ).map (pullback.fst _ _) ≫
        (gluingRecoveryFunctor ψ).map (d j k) ≫ h j =
    (gluingRecoveryFunctor ψ).map (pullback.fst _ _) ≫
      (gluingRecoveryFunctor ψ).map (d i j) ≫ h i
theorem

rawGluingTripleTransition_cocycle

L149 ↗
EtaleFundamentalGroups.rawGluingTripleTransition_cocycle
Source context 19 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable {B' Z : Scheme.{u}} (ψ : B' ⟶ B)
local instance gluingRecoveryFunctor_faithful [Flat ψ] [Surjective ψ] :
    (gluingRecoveryFunctor ψ).Faithful := by
  let : ∀ (T : Scheme.{u}) (g : T ⟶ B), Epi (pullback.fst g ψ) :=
    fun T g => Flat.epi_of_flat_of_surjective (pullback.fst g ψ)
  infer_instance
variable (h : ∀ i : 𝒰.I₀, (gluingRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (gluingRecoveryFunctor ψ).map (t i j) ≫ (gluingRecoveryFunctor ψ).map (d j i) ≫ h j =
    (gluingRecoveryFunctor ψ).map (d i j) ≫ h i)
variable (hinj : ∀ (T : Over B) (i j : 𝒰.I₀),
  Function.Injective ((gluingRecoveryFunctor ψ).map (X := T) (Y := V (i, j))))
include hrec hinj in
Lean source · statement
theorem rawGluingTripleTransition_cocycle (i j k : 𝒰.I₀) :
    rawGluingTripleTransition 𝒰 A V d y ℓ hV t ht i j k ≫
      rawGluingTripleTransition 𝒰 A V d y ℓ hV t ht j k i ≫
        rawGluingTripleTransition 𝒰 A V d y ℓ hV t ht k i j = 𝟙 _
def

finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective

L167 ↗
EtaleFundamentalGroups.finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective
Documentation

Actual cartesian overlaps and recovered transitions produce scheme gluing data, with the diagonal and triple cocycle laws proved by injectivity into the actual overlaps.

Source context 18 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable {B' Z : Scheme.{u}} (ψ : B' ⟶ B)
local instance gluingRecoveryFunctor_faithful [Flat ψ] [Surjective ψ] :
    (gluingRecoveryFunctor ψ).Faithful := by
  let : ∀ (T : Scheme.{u}) (g : T ⟶ B), Epi (pullback.fst g ψ) :=
    fun T g => Flat.epi_of_flat_of_surjective (pullback.fst g ψ)
  infer_instance
variable (h : ∀ i : 𝒰.I₀, (gluingRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (gluingRecoveryFunctor ψ).map (t i j) ≫ (gluingRecoveryFunctor ψ).map (d j i) ≫ h j =
    (gluingRecoveryFunctor ψ).map (d i j) ≫ h i)
variable (hinj : ∀ (T : Over B) (i j : 𝒰.I₀),
  Function.Injective ((gluingRecoveryFunctor ψ).map (X := T) (Y := V (i, j))))
Lean source · statement
def finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective : Scheme.GlueData.{u}
theorem

finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective_U

L185 ↗
EtaleFundamentalGroups.finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective_U
Documentation

The gluing data retain the actual local model objects.

Source context 18 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable {B' Z : Scheme.{u}} (ψ : B' ⟶ B)
local instance gluingRecoveryFunctor_faithful [Flat ψ] [Surjective ψ] :
    (gluingRecoveryFunctor ψ).Faithful := by
  let : ∀ (T : Scheme.{u}) (g : T ⟶ B), Epi (pullback.fst g ψ) :=
    fun T g => Flat.epi_of_flat_of_surjective (pullback.fst g ψ)
  infer_instance
variable (h : ∀ i : 𝒰.I₀, (gluingRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (gluingRecoveryFunctor ψ).map (t i j) ≫ (gluingRecoveryFunctor ψ).map (d j i) ≫ h j =
    (gluingRecoveryFunctor ψ).map (d i j) ≫ h i)
variable (hinj : ∀ (T : Over B) (i j : 𝒰.I₀),
  Function.Injective ((gluingRecoveryFunctor ψ).map (X := T) (Y := V (i, j))))
Lean source · statement
theorem finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective_U (i : 𝒰.I₀) :
    (finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective
      𝒰 A V d y ℓ hV t ht ψ h hrec hinj).U i =
      (A i).left
theorem

finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective_f

L191 ↗
EtaleFundamentalGroups.finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective_f
Documentation

The gluing data retain the actual overlap inclusions.

Source context 18 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable {B' Z : Scheme.{u}} (ψ : B' ⟶ B)
local instance gluingRecoveryFunctor_faithful [Flat ψ] [Surjective ψ] :
    (gluingRecoveryFunctor ψ).Faithful := by
  let : ∀ (T : Scheme.{u}) (g : T ⟶ B), Epi (pullback.fst g ψ) :=
    fun T g => Flat.epi_of_flat_of_surjective (pullback.fst g ψ)
  infer_instance
variable (h : ∀ i : 𝒰.I₀, (gluingRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (gluingRecoveryFunctor ψ).map (t i j) ≫ (gluingRecoveryFunctor ψ).map (d j i) ≫ h j =
    (gluingRecoveryFunctor ψ).map (d i j) ≫ h i)
variable (hinj : ∀ (T : Over B) (i j : 𝒰.I₀),
  Function.Injective ((gluingRecoveryFunctor ψ).map (X := T) (Y := V (i, j))))
Lean source · statement
theorem finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective_f (i j : 𝒰.I₀) :
    (finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective
      𝒰 A V d y ℓ hV t ht ψ h hrec hinj).f i j =
      (d i j).left
theorem

finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective_t

L197 ↗
EtaleFundamentalGroups.finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective_t
Documentation

The gluing data retain the actually descended transition maps.

Source context 18 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable {B' Z : Scheme.{u}} (ψ : B' ⟶ B)
local instance gluingRecoveryFunctor_faithful [Flat ψ] [Surjective ψ] :
    (gluingRecoveryFunctor ψ).Faithful := by
  let : ∀ (T : Scheme.{u}) (g : T ⟶ B), Epi (pullback.fst g ψ) :=
    fun T g => Flat.epi_of_flat_of_surjective (pullback.fst g ψ)
  infer_instance
variable (h : ∀ i : 𝒰.I₀, (gluingRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (gluingRecoveryFunctor ψ).map (t i j) ≫ (gluingRecoveryFunctor ψ).map (d j i) ≫ h j =
    (gluingRecoveryFunctor ψ).map (d i j) ≫ h i)
variable (hinj : ∀ (T : Over B) (i j : 𝒰.I₀),
  Function.Injective ((gluingRecoveryFunctor ψ).map (X := T) (Y := V (i, j))))
Lean source · statement
theorem finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective_t (i j : 𝒰.I₀) :
    (finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective
      𝒰 A V d y ℓ hV t ht ψ h hrec hinj).t i j =
      (t i j).left
theorem

exists_finiteEtale_fromRecoveredTransitionsOfOverlapInjective

L204 ↗
EtaleFundamentalGroups.exists_finiteEtale_fromRecoveredTransitionsOfOverlapInjective
Documentation

Recovered transitions glue the actual finite étale local models to an actual finite étale scheme over the covered base.

Source context 18 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable {B' Z : Scheme.{u}} (ψ : B' ⟶ B)
local instance gluingRecoveryFunctor_faithful [Flat ψ] [Surjective ψ] :
    (gluingRecoveryFunctor ψ).Faithful := by
  let : ∀ (T : Scheme.{u}) (g : T ⟶ B), Epi (pullback.fst g ψ) :=
    fun T g => Flat.epi_of_flat_of_surjective (pullback.fst g ψ)
  infer_instance
variable (h : ∀ i : 𝒰.I₀, (gluingRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (gluingRecoveryFunctor ψ).map (t i j) ≫ (gluingRecoveryFunctor ψ).map (d j i) ≫ h j =
    (gluingRecoveryFunctor ψ).map (d i j) ≫ h i)
variable (hinj : ∀ (T : Over B) (i j : 𝒰.I₀),
  Function.Injective ((gluingRecoveryFunctor ψ).map (X := T) (Y := V (i, j))))
Lean source · statement
theorem exists_finiteEtale_fromRecoveredTransitionsOfOverlapInjective
    [∀ i : 𝒰.I₀, IsFiniteEtale (y i)] :
    ∃ q : (finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective
      𝒰 A V d y ℓ hV t ht ψ h hrec hinj).glued ⟶ S,
      IsFiniteEtale q ∧ ∀ i : 𝒰.I₀,
        IsPullback (y i)
          ((finiteStageGlueDataOfRecoveredTransitionsOfOverlapInjective
            𝒰 A V d y ℓ hV t ht ψ h hrec hinj).ι i)
          (𝒰.f i) q
abbrev

finiteStageGlueDataOfRecoveredTransitions

L225 ↗
EtaleFundamentalGroups.finiteStageGlueDataOfRecoveredTransitions
Documentation

Actual cartesian overlaps and recovered transitions produce scheme gluing data, with the diagonal and triple cocycle laws proved by faithful pullback.

Source context 19 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable {B' Z : Scheme.{u}} (ψ : B' ⟶ B)
local instance gluingRecoveryFunctor_faithful [Flat ψ] [Surjective ψ] :
    (gluingRecoveryFunctor ψ).Faithful := by
  let : ∀ (T : Scheme.{u}) (g : T ⟶ B), Epi (pullback.fst g ψ) :=
    fun T g => Flat.epi_of_flat_of_surjective (pullback.fst g ψ)
  infer_instance
variable (h : ∀ i : 𝒰.I₀, (gluingRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (gluingRecoveryFunctor ψ).map (t i j) ≫ (gluingRecoveryFunctor ψ).map (d j i) ≫ h j =
    (gluingRecoveryFunctor ψ).map (d i j) ≫ h i)
variable (hinj : ∀ (T : Over B) (i j : 𝒰.I₀),
  Function.Injective ((gluingRecoveryFunctor ψ).map (X := T) (Y := V (i, j))))
variable [Flat ψ] [Surjective ψ]
Lean source · statement
abbrev finiteStageGlueDataOfRecoveredTransitions : Scheme.GlueData.{u}
theorem

finiteStageGlueDataOfRecoveredTransitions_U

L230 ↗
EtaleFundamentalGroups.finiteStageGlueDataOfRecoveredTransitions_U
Documentation

The gluing data retain the actual local model objects.

Source context 19 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable {B' Z : Scheme.{u}} (ψ : B' ⟶ B)
local instance gluingRecoveryFunctor_faithful [Flat ψ] [Surjective ψ] :
    (gluingRecoveryFunctor ψ).Faithful := by
  let : ∀ (T : Scheme.{u}) (g : T ⟶ B), Epi (pullback.fst g ψ) :=
    fun T g => Flat.epi_of_flat_of_surjective (pullback.fst g ψ)
  infer_instance
variable (h : ∀ i : 𝒰.I₀, (gluingRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (gluingRecoveryFunctor ψ).map (t i j) ≫ (gluingRecoveryFunctor ψ).map (d j i) ≫ h j =
    (gluingRecoveryFunctor ψ).map (d i j) ≫ h i)
variable (hinj : ∀ (T : Over B) (i j : 𝒰.I₀),
  Function.Injective ((gluingRecoveryFunctor ψ).map (X := T) (Y := V (i, j))))
variable [Flat ψ] [Surjective ψ]
Lean source · statement
theorem finiteStageGlueDataOfRecoveredTransitions_U (i : 𝒰.I₀) :
    (finiteStageGlueDataOfRecoveredTransitions 𝒰 A V d y ℓ hV t ht ψ h hrec).U i =
      (A i).left
theorem

finiteStageGlueDataOfRecoveredTransitions_f

L235 ↗
EtaleFundamentalGroups.finiteStageGlueDataOfRecoveredTransitions_f
Documentation

The gluing data retain the actual overlap inclusions.

Source context 19 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable {B' Z : Scheme.{u}} (ψ : B' ⟶ B)
local instance gluingRecoveryFunctor_faithful [Flat ψ] [Surjective ψ] :
    (gluingRecoveryFunctor ψ).Faithful := by
  let : ∀ (T : Scheme.{u}) (g : T ⟶ B), Epi (pullback.fst g ψ) :=
    fun T g => Flat.epi_of_flat_of_surjective (pullback.fst g ψ)
  infer_instance
variable (h : ∀ i : 𝒰.I₀, (gluingRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (gluingRecoveryFunctor ψ).map (t i j) ≫ (gluingRecoveryFunctor ψ).map (d j i) ≫ h j =
    (gluingRecoveryFunctor ψ).map (d i j) ≫ h i)
variable (hinj : ∀ (T : Over B) (i j : 𝒰.I₀),
  Function.Injective ((gluingRecoveryFunctor ψ).map (X := T) (Y := V (i, j))))
variable [Flat ψ] [Surjective ψ]
Lean source · statement
theorem finiteStageGlueDataOfRecoveredTransitions_f (i j : 𝒰.I₀) :
    (finiteStageGlueDataOfRecoveredTransitions 𝒰 A V d y ℓ hV t ht ψ h hrec).f i j =
      (d i j).left
theorem

finiteStageGlueDataOfRecoveredTransitions_t

L240 ↗
EtaleFundamentalGroups.finiteStageGlueDataOfRecoveredTransitions_t
Documentation

The gluing data retain the actually descended transition maps.

Source context 19 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable {B' Z : Scheme.{u}} (ψ : B' ⟶ B)
local instance gluingRecoveryFunctor_faithful [Flat ψ] [Surjective ψ] :
    (gluingRecoveryFunctor ψ).Faithful := by
  let : ∀ (T : Scheme.{u}) (g : T ⟶ B), Epi (pullback.fst g ψ) :=
    fun T g => Flat.epi_of_flat_of_surjective (pullback.fst g ψ)
  infer_instance
variable (h : ∀ i : 𝒰.I₀, (gluingRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (gluingRecoveryFunctor ψ).map (t i j) ≫ (gluingRecoveryFunctor ψ).map (d j i) ≫ h j =
    (gluingRecoveryFunctor ψ).map (d i j) ≫ h i)
variable (hinj : ∀ (T : Over B) (i j : 𝒰.I₀),
  Function.Injective ((gluingRecoveryFunctor ψ).map (X := T) (Y := V (i, j))))
variable [Flat ψ] [Surjective ψ]
Lean source · statement
theorem finiteStageGlueDataOfRecoveredTransitions_t (i j : 𝒰.I₀) :
    (finiteStageGlueDataOfRecoveredTransitions 𝒰 A V d y ℓ hV t ht ψ h hrec).t i j =
      (t i j).left
theorem

exists_finiteEtale_fromRecoveredTransitions

L246 ↗
EtaleFundamentalGroups.exists_finiteEtale_fromRecoveredTransitions
Documentation

Recovered transitions glue the actual finite étale local models to an actual finite étale scheme over the covered base.

Source context 19 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {B S : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over B) (V : 𝒰.I₀ × 𝒰.I₀ → Over B)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable {B' Z : Scheme.{u}} (ψ : B' ⟶ B)
local instance gluingRecoveryFunctor_faithful [Flat ψ] [Surjective ψ] :
    (gluingRecoveryFunctor ψ).Faithful := by
  let : ∀ (T : Scheme.{u}) (g : T ⟶ B), Epi (pullback.fst g ψ) :=
    fun T g => Flat.epi_of_flat_of_surjective (pullback.fst g ψ)
  infer_instance
variable (h : ∀ i : 𝒰.I₀, (gluingRecoveryFunctor ψ).obj (A i) ⟶ Z)
variable [∀ i : 𝒰.I₀, Mono (h i)]
variable (hrec : ∀ i j : 𝒰.I₀,
  (gluingRecoveryFunctor ψ).map (t i j) ≫ (gluingRecoveryFunctor ψ).map (d j i) ≫ h j =
    (gluingRecoveryFunctor ψ).map (d i j) ≫ h i)
variable (hinj : ∀ (T : Over B) (i j : 𝒰.I₀),
  Function.Injective ((gluingRecoveryFunctor ψ).map (X := T) (Y := V (i, j))))
variable [Flat ψ] [Surjective ψ]
Lean source · statement
theorem exists_finiteEtale_fromRecoveredTransitions [∀ i : 𝒰.I₀, IsFiniteEtale (y i)] :
    ∃ q : (finiteStageGlueDataOfRecoveredTransitions 𝒰 A V d y ℓ hV t ht ψ h hrec).glued ⟶ S,
      IsFiniteEtale q ∧ ∀ i : 𝒰.I₀,
        IsPullback (y i)
          ((finiteStageGlueDataOfRecoveredTransitions 𝒰 A V d y ℓ hV t ht ψ h hrec).ι i)
          (𝒰.f i) q

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