English
The right triangle identity is satisfied in the Γ-Spec adjunction for all R.
Русский
Правая треугольная идентичность выполняется для всех R.
LaTeX
$$Γ_Spec_right_triangle_part := ...$$
Lean4
/-- The unit as a natural transformation. -/
def identityToΓSpec : 𝟭 LocallyRingedSpace.{u} ⟶ Γ.rightOp ⋙ Spec.toLocallyRingedSpace
where
app := LocallyRingedSpace.toΓSpec
naturality X Y
f := by
symm
apply LocallyRingedSpace.comp_ring_hom_ext
· ext1 x
dsimp
change PrimeSpectrum.comap (f.c.app (op ⊤)).hom (X.toΓSpecFun x) = Y.toΓSpecFun (f.base x)
dsimp [toΓSpecFun]
rw [← IsLocalRing.comap_closedPoint (f.stalkMap x).hom, ← PrimeSpectrum.comap_comp_apply, ←
PrimeSpectrum.comap_comp_apply, ← CommRingCat.hom_comp, ← CommRingCat.hom_comp]
congr 3
exact (PresheafedSpace.stalkMap_germ f.1 ⊤ x trivial).symm
· intro r
rw [LocallyRingedSpace.comp_c_app, ← Category.assoc]
erw [Y.toΓSpecSheafedSpace_app_spec, f.c.naturality]
rfl
