liftQuotient_comp — Mathlib

English

The appTop map of the factorization of f into SpecTargetImage is injective.

Русский

Отображение appTop факторизации f в SpecTargetImage инъективно.

LaTeX

$$specTargetImageFactorization f).appTop is injective$$

Lean4

@[reassoc]
theorem liftQuotient_comp (f : X.Hom (Spec A)) (I : Ideal A)
    (hI : I ≤ RingHom.ker ((Scheme.ΓSpecIso A).inv ≫ f.appTop).hom) :
    f.liftQuotient I hI ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk _)) = f :=
  by
  rw [Scheme.Hom.liftQuotient, Category.assoc, ← Spec.map_comp, ← CommRingCat.ofHom_comp, Ideal.Quotient.lift_comp_mk]
  simp only [CommRingCat.hom_comp, CommRingCat.ofHom_comp, CommRingCat.ofHom_hom, Spec.map_comp,
    ← Scheme.toSpecΓ_naturality_assoc, ← SpecMap_ΓSpecIso_hom]
  simp only [← Spec.map_comp, Iso.inv_hom_id, Spec.map_id, Category.comp_id]

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