English
An explicit compatibility between the inverse of the refinement isomorphism and pullback maps is given by a natural pullback equality.
Русский
Явно указана совместимость обратного изоморфизма уточнения с тягодравлями, выраженная равенством на pullback.
LaTeX
$$$$ (\mathcal{U}.pullbackCoverAffineRefinementObjIso f 𝒰 i)^{-1} \\circ (\mathcal{U}.affineRefinement.openCover.pullbackHom f i) = \\circ ((\mathcal{U}.X i.1).affineCover.pullbackHom (\mathcal{U}.pullbackHom f i.1)) i.2 $$$$
Lean4
@[reassoc]
theorem pullbackCoverAffineRefinementObjIso_inv_map (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i) :
(𝒰.pullbackCoverAffineRefinementObjIso f i).inv ≫ (𝒰.affineRefinement.openCover.pullback₁ f).f i =
((𝒰.X i.1).affineCover.pullback₁ (𝒰.pullbackHom f i.1)).f i.2 ≫ (𝒰.pullback₁ f).f i.1 :=
by
simp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover, PreZeroHypercover.pullback₁_X,
AffineOpenCover.openCover_X, AffineOpenCover.openCover_f, pullbackCoverAffineRefinementObjIso, Iso.trans_inv,
asIso_inv, Iso.symm_inv, Category.assoc, PreZeroHypercover.pullback₁_f, pullbackSymmetry_inv_comp_fst,
IsIso.inv_comp_eq, limit.lift_π_assoc, PullbackCone.mk_pt, cospan_left, PullbackCone.mk_π_app,
pullbackSymmetry_hom_comp_fst]
convert pullbackSymmetry_inv_comp_snd_assoc ((𝒰.X i.1).affineCover.f i.2) (pullback.fst _ _) _ using 2
exact pullbackRightPullbackFstIso_hom_snd _ _ _
