Lean4
/-- The glued scheme (`(gluing 𝒰 f g).glued`) is indeed the pullback of `f` and `g`. -/
def gluedIsLimit : IsLimit (PullbackCone.mk _ _ (p_comm 𝒰 f g)) :=
by
apply PullbackCone.isLimitAux'
intro s
refine ⟨gluedLift 𝒰 f g s, gluedLift_p1 𝒰 f g s, gluedLift_p2 𝒰 f g s, ?_⟩
intro m h₁ h₂
simp_rw [PullbackCone.mk_pt, PullbackCone.mk_π_app] at h₁ h₂
apply Cover.hom_ext <| 𝒰.pullback₁ s.fst
intro i
rw [gluedLift, (Cover.ι_glueMorphisms <| 𝒰.pullback₁ s.fst)]
dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover, PreZeroHypercover.pullback₁_X,
PullbackCone.mk_pt, PreZeroHypercover.pullback₁_f, gluing_ι]
rw [← cancel_epi (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m ≪≫ pullback.congrHom h₁ rfl).hom, Iso.trans_hom,
Category.assoc, pullback.congrHom_hom, pullback.lift_fst_assoc, Category.comp_id,
pullbackRightPullbackFstIso_hom_fst_assoc, pullback.condition]
conv_lhs => rhs; rw [← pullbackP1Iso_hom_ι]
simp_rw [← Category.assoc]
congr 1
apply pullback.hom_ext
·
simp_rw [Category.assoc, pullbackP1Iso_hom_fst, pullback.lift_fst, Category.comp_id, pullbackSymmetry_hom_comp_fst,
pullback.lift_snd, Category.comp_id, pullbackRightPullbackFstIso_hom_snd]
·
simp_rw [Category.assoc, pullbackP1Iso_hom_snd, pullback.lift_snd, pullbackSymmetry_hom_comp_snd_assoc,
pullback.lift_fst_assoc, Category.comp_id, pullbackRightPullbackFstIso_hom_fst_assoc, ← pullback.condition_assoc,
h₂]
