AlgebraicGeometry.Scheme.Cover.recoveredPullbackTransition_isPullback
The actual recovered raw overlap is the pullback of the two recovered chart maps into the original scheme, for an arbitrary base change.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.CoverLean source · statement
theorem recoveredPullbackTransition_isPullback
{S L : Scheme.{u}} (ψ : L ⟶ S) (𝒰 : S.OpenCover.{u})
(M : ∀ i : 𝒰.I₀, Over (𝒰.X i)) (Z : Over L)
(e : ∀ i : 𝒰.I₀,
(Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
(Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
(i j : 𝒰.I₀) :
IsPullback ((Over.pullback ψ).map (gluingOverlapFirst 𝒰 M i j)).left
(recoveredPullbackTransition ψ 𝒰 M Z e i j ≫
(Over.pullback ψ).map (gluingOverlapFirst 𝒰 M j i)).left
(recoveredPullbackChartMap ψ 𝒰 M Z e i)
(recoveredPullbackChartMap ψ 𝒰 M Z e j)