specTargetImageFactorization_app_injective

English

The appTop component of the target image factorization is injective.

Русский

Компонента appTop факторизации целевого изображения инъективна.

LaTeX

$$$ \text{Injective} \left| (\mathrm{specTargetImageFactorization} f).appTop \right.$$$

Lean4

theorem specTargetImageFactorization_app_injective : Function.Injective <| (specTargetImageFactorization f).appTop :=
  by
  let φ : A ⟶ Γ(X, ⊤) := (((ΓSpec.adjunction).homEquiv X (op A)).symm f).unop
  let φ' : specTargetImage f ⟶ Scheme.Γ.obj (op X) := CommRingCat.ofHom (RingHom.kerLift φ.hom)
  change Function.Injective <| ((ΓSpec.adjunction.homEquiv X _) φ'.op).appTop
  rw [ΓSpec_adjunction_homEquiv_eq]
  apply (RingHom.kerLift_injective φ.hom).comp
  exact ((ConcreteCategory.isIso_iff_bijective (Scheme.ΓSpecIso _).hom).mp inferInstance).injective

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