English
There exists a canonical lift from the fiber product W ×_X U_i to U_i ×_Z Y such that composing with the gluing morphism recovers the natural first projection from the pullback over X.
Русский
Существуют канонические отображения, связывающие fibration и проекции; подъём из W ×_X U_i в U_i ×_Z Y, при композиции с склейкой даёт естественную первую проекцию из вытянутого на X-над-Зpulback.
LaTeX
$$$$ (\text{lift})_{i} \;:\; \mathrm{pullback}( \mathrm{snd}, \mathrm{fst} \circ p_2) \; \longrightarrow \mathrm{pullback}(p_1, f) $$
$$ \text{(gluing 𝒰 f g)}_i \;\circ\; \text{lift} = \mathrm{fst}_{(p_1 𝒰 f g, 𝒰.f i)} $$$$
Lean4
/-- We show that the map `W ×[X] Uᵢ ⟶ Uᵢ ×[Z] Y ⟶ W` is the first projection, where the
first map is given by the lift of `W ×[X] Uᵢ ⟶ Uᵢ` and `W ×[X] Uᵢ ⟶ W ⟶ Y`.
It suffices to show that the two map agrees when restricted onto `Uⱼ ×[Z] Y`. In this case,
both maps factor through `V j i` via `pullback_fst_ι_to_V` -/
theorem lift_comp_ι (i : 𝒰.I₀) :
pullback.lift (pullback.snd _ _) (pullback.fst _ _ ≫ p2 𝒰 f g)
(by rw [← pullback.condition_assoc, Category.assoc, p_comm]) ≫
(gluing 𝒰 f g).ι i =
(pullback.fst _ _ : pullback (p1 𝒰 f g) (𝒰.f i) ⟶ _) :=
by
apply Cover.hom_ext ((gluing 𝒰 f g).openCover.pullback₁ (pullback.fst _ _))
intro j
dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover, PreZeroHypercover.pullback₁_X,
PreZeroHypercover.pullback₁_f]
trans pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι _
· rw [← show _ = fV 𝒰 f g j i ≫ _ from (gluing 𝒰 f g).glue_condition j i]
simp_rw [← Category.assoc]
congr 1
rw [gluing_f, gluing_t]
apply pullback.hom_ext <;> simp_rw [Category.assoc]
· simp_rw [t_fst_fst, pullback.lift_fst, pullbackFstιToV_snd, GlueData.openCover_f]
· simp_rw [t_fst_snd, pullback.lift_snd, pullbackFstιToV_fst_assoc, pullback.condition_assoc, GlueData.openCover_f,
p2]
simp
· rw [pullback.condition, ← Category.assoc]
simp_rw [pullbackFstιToV_fst, GlueData.openCover_f]
