AlgebraicGeometry.surjective_closedFiber_appTop_of_isProper_of_isFiniteSplit
Proper idempotent lifting supplies surjectivity on sections when the actual closed-fibre algebra is finite split.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe uLean source · full declaration
theorem surjective_closedFiber_appTop_of_isProper_of_isFiniteSplit
{A : Type u} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
{X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) [IsProper f] :
let q : Spec (CommRingCat.of (IsLocalRing.ResidueField A)) ⟶ Spec (CommRingCat.of A) :=
Spec.map (CommRingCat.ofHom (IsLocalRing.residue A))
let : Algebra (IsLocalRing.ResidueField A) Γ(pullback f q, ⊤) :=
((Scheme.ΓSpecIso (CommRingCat.of (IsLocalRing.ResidueField A))).inv ≫
(pullback.snd f q).appTop).hom.toAlgebra
Algebra.IsFiniteSplit (IsLocalRing.ResidueField A) Γ(pullback f q, ⊤) →
Function.Surjective (pullback.fst f q).appTop := by
intro q hκ hSplit
let : Algebra A Γ(X, ⊤) :=
((Scheme.ΓSpecIso (CommRingCat.of A)).inv ≫ f.appTop).hom.toAlgebra
let : Algebra A Γ(pullback f q, ⊤) :=
Algebra.compHom Γ(pullback f q, ⊤) (IsLocalRing.residue A)
have : IsScalarTower A (IsLocalRing.ResidueField A) Γ(pullback f q, ⊤) :=
IsScalarTower.of_algebraMap_eq' rfl
let ψ : Γ(X, ⊤) →ₐ[A] Γ(pullback f q, ⊤) :=
{ toRingHom := (pullback.fst f q).appTop.hom
commutes' := fun a => by
change (((Scheme.ΓSpecIso (CommRingCat.of A)).inv ≫ f.appTop) ≫
(pullback.fst f q).appTop) a =
(CommRingCat.ofHom (IsLocalRing.residue A) ≫
(Scheme.ΓSpecIso (CommRingCat.of (IsLocalRing.ResidueField A))).inv ≫
(pullback.snd f q).appTop) a
congr 2
rw [Category.assoc, ← Scheme.Hom.comp_appTop, pullback.condition,
Scheme.Hom.comp_appTop, ← Scheme.ΓSpecIso_inv_naturality_assoc] }
apply Algebra.surjective_of_isFiniteSplit_of_idempotents_mem_range
ψ IsLocalRing.residue_surjective
intro e he
obtain ⟨a, ha⟩ := exists_appTop_eq_of_isProper_of_isIdempotentElem
f (IsLocalRing.maximalIdeal A) e he
exact ⟨a, ha⟩