exists_lift_of_germInjective_aux — Mathlib

English

Auxiliary lemma giving a lift of morphisms through germs over an expanded open set.

Русский

Лемма-помощник о подъёме отображений через герах над расширенным открытым множеством.

LaTeX

$$$\exists V \; hxV \; φ' \; i : V ≤ U \land \text{affine and lift conditions}$$$

Lean4

theorem exists_lift_of_germInjective_aux {U : X.Opens} {x : X} (hxU) (φ : 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), V ≤ U ∧ RingHom.range φ.hom ≤ RingHom.range (X.presheaf.germ V x hxV).hom :=
  by
  letI := φRA.hom.toAlgebra
  obtain ⟨s, hs⟩ := hφRA
  choose W hxW f hf using fun t ↦ X.presheaf.germ_exist x (φ t)
  have H : x ∈ s.inf W ⊓ U :=
    by
    rw [← SetLike.mem_coe, TopologicalSpace.Opens.coe_inf, TopologicalSpace.Opens.coe_finset_inf]
    exact ⟨by simpa using fun x _ ↦ hxW x, hxU⟩
  refine ⟨s.inf W ⊓ U, H, inf_le_right, ?_⟩
  letI := φRX.hom.toAlgebra
  letI := (φRX ≫ X.presheaf.germ U x hxU).hom.toAlgebra
  letI := (φRX ≫ X.presheaf.map (homOfLE (inf_le_right (a := s.inf W))).op).hom.toAlgebra
  let φ' : A →ₐ[R] X.presheaf.stalk x :=
    { φ.hom with commutes' := DFunLike.congr_fun (congr_arg CommRingCat.Hom.hom e) }
  let ψ : Γ(X, s.inf W ⊓ U) →ₐ[R] X.presheaf.stalk x :=
    { (X.presheaf.germ _ x H).hom with commutes' := fun x ↦ X.presheaf.germ_res_apply _ _ _ _ }
  change AlgHom.range φ' ≤ AlgHom.range ψ
  rw [← Algebra.map_top, ← hs, AlgHom.map_adjoin, Algebra.adjoin_le_iff]
  rintro _ ⟨i, hi, rfl : φ i = _⟩
  refine ⟨X.presheaf.map (homOfLE (inf_le_left.trans (Finset.inf_le hi))).op (f i), ?_⟩
  exact (X.presheaf.germ_res_apply _ _ _ _).trans (hf _)

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