The threefold fiber product is viewed as two copies of X ×[Y] X with their first coordinates identified. Its small diagonal is the composite of two diagonals. Both are surjective closed immersions for a separated universally injective morphism. Faithfulness along this small diagonal detects the cocycle equation.
The threefold fiber product, with the first coordinate shared by the two pairs.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}def radicialTriple (f : X ⟶ Y) : Scheme.{u}The small diagonal in the chosen threefold fiber product.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}def radicialTripleDiagonal (f : X ⟶ Y) : X ⟶ radicialTriple fThe small diagonal is a closed immersion when the original map is separated.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}instance (f : X ⟶ Y) [IsSeparated f] : IsClosedImmersion (radicialTripleDiagonal f)Universal injectivity makes the small diagonal surjective.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}instance (f : X ⟶ Y) [UniversallyInjective f] : Surjective (radicialTripleDiagonal f)The map from the pullback of V along a to its pullback along the first projection of the fiber product, induced by the pair a and b over Y.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}def pairLift (f : X ⟶ Y) (V : Over X)
(a b : T ⟶ X) (w : a ≫ f = b ≫ f) :
((Over.pullback a).obj V).left ⟶
((Over.pullback (Limits.pullback.fst f f)).obj V).leftSurrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}lemma pairLift_fst (f : X ⟶ Y) (V : Over X)
(a b : T ⟶ X) (w : a ≫ f = b ≫ f) :
pairLift f V a b w ≫ Limits.pullback.fst V.hom (Limits.pullback.fst f f) =
Limits.pullback.fst V.hom aSurrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}lemma pairLift_snd (f : X ⟶ Y) (V : Over X)
(a b : T ⟶ X) (w : a ≫ f = b ≫ f) :
pairLift f V a b w ≫ Limits.pullback.snd V.hom (Limits.pullback.fst f f) =
Limits.pullback.snd V.hom a ≫ Limits.pullback.lift a b wReindex a morphism between the two pullbacks to a pair of maps with the same composite to the base. This uses the actual universal pullback maps.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}def pairHom (f : X ⟶ Y) (V : Over X)
(η : (Over.pullback (Limits.pullback.fst f f)).obj V ⟶
(Over.pullback (Limits.pullback.snd f f)).obj V)
(a b : T ⟶ X) (w : a ≫ f = b ≫ f) :
(Over.pullback a).obj V ⟶ (Over.pullback b).obj VSurrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}lemma pairHom_fst (f : X ⟶ Y) (V : Over X)
(η : (Over.pullback (Limits.pullback.fst f f)).obj V ⟶
(Over.pullback (Limits.pullback.snd f f)).obj V)
(a b : T ⟶ X) (w : a ≫ f = b ≫ f) :
(pairHom f V η a b w).left ≫ Limits.pullback.fst V.hom b =
pairLift f V a b w ≫ η.left ≫
Limits.pullback.fst V.hom (Limits.pullback.snd f f)Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}lemma pairHom_snd (f : X ⟶ Y) (V : Over X)
(η : (Over.pullback (Limits.pullback.fst f f)).obj V ⟶
(Over.pullback (Limits.pullback.snd f f)).obj V)
(a b : T ⟶ X) (w : a ≫ f = b ≫ f) :
(pairHom f V η a b w).left ≫ Limits.pullback.snd V.hom b =
Limits.pullback.snd V.hom aThe canonical comparison on any pair of maps into X over Y.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}def radicialDescentHom (f : X ⟶ Y) [IsSeparated f] [UniversallyInjective f]
(V : finiteEtaleProperty.Over ⊤ X) (a b : T ⟶ X) (w : a ≫ f = b ≫ f) :
(Over.pullback a).obj V.toComma ⟶ (Over.pullback b).obj V.toCommaSurrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}def restrictionSection (V : Over X) (d : X ⟶ T) (a : T ⟶ X)
(ha : d ≫ a = 𝟙 X) : V.left ⟶ ((Over.pullback a).obj V).leftSurrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}lemma restrictionSection_fst (V : Over X) (d : X ⟶ T) (a : T ⟶ X)
(ha : d ≫ a = 𝟙 X) :
restrictionSection V d a ha ≫ Limits.pullback.fst V.hom a = 𝟙 V.leftSurrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}lemma restrictionSection_snd (V : Over X) (d : X ⟶ T) (a : T ⟶ X)
(ha : d ≫ a = 𝟙 X) :
restrictionSection V d a ha ≫ Limits.pullback.snd V.hom a = V.hom ≫ dSurrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}lemma restrictionSection_pairLift (f : X ⟶ Y) (V : Over X)
(d : X ⟶ T) (a b : T ⟶ X) (w : a ≫ f = b ≫ f)
(ha : d ≫ a = 𝟙 X) (hb : d ≫ b = 𝟙 X) :
restrictionSection V d a ha ≫ pairLift f V a b w =
restrictionSection V (Limits.pullback.diagonal f) (Limits.pullback.fst f f)
(Limits.pullback.diagonal_fst f)Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}lemma pairHom_restrictionSection (f : X ⟶ Y) (V : Over X)
(η : (Over.pullback (Limits.pullback.fst f f)).obj V ⟶
(Over.pullback (Limits.pullback.snd f f)).obj V)
(hη : restrictionSection V (Limits.pullback.diagonal f) (Limits.pullback.fst f f)
(Limits.pullback.diagonal_fst f) ≫ η.left =
restrictionSection V (Limits.pullback.diagonal f) (Limits.pullback.snd f f)
(Limits.pullback.diagonal_snd f))
(d : X ⟶ T) (a b : T ⟶ X) (w : a ≫ f = b ≫ f)
(ha : d ≫ a = 𝟙 X) (hb : d ≫ b = 𝟙 X) :
restrictionSection V d a ha ≫ (pairHom f V η a b w).left =
restrictionSection V d b hbSurrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}lemma hom_ext_of_restrictionSection (V : finiteEtaleProperty.Over ⊤ X)
(d : X ⟶ T) [IsClosedImmersion d] [Surjective d]
(a b : T ⟶ X) (ha : d ≫ a = 𝟙 X)
(g h : (Over.pullback a).obj V.toComma ⟶ (Over.pullback b).obj V.toComma)
(hgh : restrictionSection V.toComma d a ha ≫ g.left =
restrictionSection V.toComma d a ha ≫ h.left) : g = hOn the universal pair, reindexing recovers the original comparison.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}theorem radicialDescentHom_projections
(f : X ⟶ Y) [IsSeparated f] [UniversallyInjective f] (V : finiteEtaleProperty.Over ⊤ X) :
radicialDescentHom f V (Limits.pullback.fst f f) (Limits.pullback.snd f f)
Limits.pullback.condition = ((radicialDescentIso f).hom.app V).homSurrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}lemma radicialDescentHom_restrictionSection
(f : X ⟶ Y) [IsSeparated f] [UniversallyInjective f] (V : finiteEtaleProperty.Over ⊤ X)
(d : X ⟶ T) (a b : T ⟶ X) (w : a ≫ f = b ≫ f)
(ha : d ≫ a = 𝟙 X) (hb : d ≫ b = 𝟙 X) :
restrictionSection V.toComma d a ha ≫ (radicialDescentHom f V a b w).left =
restrictionSection V.toComma d b hbComparisons satisfy the cocycle whenever a surjective closed section simultaneously identifies the three coordinates with X.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}theorem radicialDescentHom_cocycle_of_section
(f : X ⟶ Y) [IsSeparated f] [UniversallyInjective f] (V : finiteEtaleProperty.Over ⊤ X)
(d : X ⟶ T) [IsClosedImmersion d] [Surjective d]
(a b c : T ⟶ X) (wab : a ≫ f = b ≫ f) (wbc : b ≫ f = c ≫ f)
(ha : d ≫ a = 𝟙 X) (hb : d ≫ b = 𝟙 X) (hc : d ≫ c = 𝟙 X) :
radicialDescentHom f V a b wab ≫ radicialDescentHom f V b c wbc =
radicialDescentHom f V a c (wab.trans wbc)The first coordinate of the threefold fiber product.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}def radicialTripleFirst (f : X ⟶ Y) : radicialTriple f ⟶ XThe second coordinate of the threefold fiber product.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}def radicialTripleSecond (f : X ⟶ Y) : radicialTriple f ⟶ XThe third coordinate of the threefold fiber product.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}def radicialTripleThird (f : X ⟶ Y) : radicialTriple f ⟶ XSurrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}theorem radicialTripleDiagonal_first (f : X ⟶ Y) :
radicialTripleDiagonal f ≫ radicialTripleFirst f = 𝟙 XSurrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}theorem radicialTripleDiagonal_second (f : X ⟶ Y) :
radicialTripleDiagonal f ≫ radicialTripleSecond f = 𝟙 XSurrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}theorem radicialTripleDiagonal_third (f : X ⟶ Y) :
radicialTripleDiagonal f ≫ radicialTripleThird f = 𝟙 XSurrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}theorem radicialTriple_first_second (f : X ⟶ Y) :
radicialTripleFirst f ≫ f = radicialTripleSecond f ≫ fSurrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}theorem radicialTriple_first_third (f : X ⟶ Y) :
radicialTripleFirst f ≫ f = radicialTripleThird f ≫ fSurrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}theorem radicialTriple_second_third (f : X ⟶ Y) :
radicialTripleSecond f ≫ f = radicialTripleThird f ≫ fThe canonical radicial comparison satisfies the cocycle on the actual threefold fiber product. The reindexed maps use universal pullback lifts.
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
variable {X Y T : Scheme.{u}}theorem radicialDescentHom_cocycle
(f : X ⟶ Y) [IsSeparated f] [UniversallyInjective f] (V : finiteEtaleProperty.Over ⊤ X) :
radicialDescentHom f V (radicialTripleFirst f) (radicialTripleSecond f)
(radicialTriple_first_second f) ≫
radicialDescentHom f V (radicialTripleSecond f) (radicialTripleThird f)
(radicialTriple_second_third f) =
radicialDescentHom f V (radicialTripleFirst f) (radicialTripleThird f)
(radicialTriple_first_third f)