locallyRingedSpaceAdjunction_homEquiv_apply'

English

Let X be a LocallyRingedSpace and R a commutative ring. For any morphism f : CommRingCat.of R ⟶ Γ.obj(op X), the homomorphism part of the Γ-Spec adjunction is given by the composite identityToΓSpec.app X ≫ Spec.locallyRingedSpaceMap f under the adjunction hom-equivalence.

Русский

Пусть X — локально кольцевая пространства, R — кольцо коммутативное. Для любого отображения f: CommRingCat.of R ⟶ Γ.obj(op X) отображение из Γ-Spec-взаимодействия гомоморфизмов задается как композиция identityToΓSpec.app X ≫ Spec.locallyRingedSpaceMap f.

LaTeX

$$$\text{locallyRingedSpaceAdjunction.homEquiv } X (op R) (op f) = \ identityToΓSpec.app X \; \gg \; Spec.locallyRingedSpaceMap f$$$

Lean4

theorem locallyRingedSpaceAdjunction_homEquiv_apply' {X : LocallyRingedSpace} {R : Type u} [CommRing R]
    (f : CommRingCat.of R ⟶ Γ.obj <| op X) :
    locallyRingedSpaceAdjunction.homEquiv X (op <| CommRingCat.of R) (op f) =
      identityToΓSpec.app X ≫ Spec.locallyRingedSpaceMap f :=
  rfl

Похожие утверждения