English
With germ-injectivity, there exists a lift (V, hxV, φ′, i) realizing the lift of the diagram through germs.
Русский
При инъективности гера существует подъём (V, hxV, φ′, i), реализующий подъем диаграммы через гера.
LaTeX
$$$\exists (V : X.Opens) (hxV : x ∈ V) (φ' : R \to Γ(X, V)) (i : V ≤ U),\ IsAffineOpen V ∧ φ = φ' \circ germ_Vx ∧ φRX \circ map i = φRA \circ φ'$$$
Lean4
/-- Suppose `X` is a scheme, `x : X` such that the germ map at `x` is (locally) injective,
and `U` is a neighborhood of `x`.
Given a commutative diagram of `CommRingCat`
```
R ⟶ Γ(X, U)
↓ ↓
A ⟶ 𝒪_{X, x}
```
such that `R` is of finite type over `A`, we may lift `A ⟶ 𝒪_{X, x}` to some `A ⟶ Γ(X, V)`.
-/
theorem exists_lift_of_germInjective {x : X} [X.IsGermInjectiveAt x] {U : X.Opens} (hxU : x ∈ U)
(φ : A ⟶ X.presheaf.stalk x) (φRA : R ⟶ A) (φRX : R ⟶ Γ(X, U)) (hφRA : RingHom.FiniteType φRA.hom)
(e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU) :
∃ (V : X.Opens) (hxV : x ∈ V) (φ' : A ⟶ Γ(X, V)) (i : V ≤ U),
IsAffineOpen V ∧ φ = φ' ≫ X.presheaf.germ V x hxV ∧ φRX ≫ X.presheaf.map i.hom.op = φRA ≫ φ' :=
by
obtain ⟨V, hxV, iVU, hV⟩ := exists_lift_of_germInjective_aux hxU φ φRA φRX hφRA e
obtain ⟨V', hxV', hV', iV'V, H⟩ := X.exists_le_and_germ_injective x V hxV
let f := X.presheaf.germ V' x hxV'
have hf' : RingHom.range (X.presheaf.germ V x hxV).hom ≤ RingHom.range f.hom :=
by
rw [← X.presheaf.germ_res iV'V.hom _ hxV']
exact Set.range_comp_subset_range (X.presheaf.map iV'V.hom.op) f
let e := RingEquiv.ofLeftInverse H.hasLeftInverse.choose_spec
refine
⟨V', hxV', CommRingCat.ofHom (e.symm.toRingHom.comp (φ.hom.codRestrict _ (fun x ↦ hf' (hV ⟨x, rfl⟩)))),
iV'V.trans iVU, hV', ?_, ?_⟩
· ext a
change φ a = (e (e.symm _)).1
simp only [RingEquiv.apply_symm_apply]
rfl
· ext a
apply e.injective
change e _ = e (e.symm _)
rw [RingEquiv.apply_symm_apply]
ext
change X.presheaf.germ _ _ _ (X.presheaf.map _ _) = (φRA ≫ φ) a
rw [TopCat.Presheaf.germ_res_apply, ‹φRA ≫ φ = _›]
rfl
