AlgebraicGeometry.Scheme.exists_isAlgClosed_factor_residueField_of_range_subset_singleton
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isAlgClosed_factor_residueField_of_range_subset_singleton
universe u
open CategoryTheory AlgebraicGeometryLean source · statement
theorem
_root_.AlgebraicGeometry.Scheme.exists_isAlgClosed_factor_residueField_of_range_subset_singleton
{T : Scheme.{u}} (x : T)
{k₁ : Type u} [Field k₁] (s₁ : Spec (CommRingCat.of k₁) ⟶ T) (hs₁ : Set.range ⇑s₁ ⊆ {x})
{k₂ : Type u} [Field k₂] (s₂ : Spec (CommRingCat.of k₂) ⟶ T) (hs₂ : Set.range ⇑s₂ ⊆ {x}) :
∃ (ι₁ : T.residueField x ⟶ CommRingCat.of k₁) (ι₂ : T.residueField x ⟶ CommRingCat.of k₂)
(Ω : Type u) (_ : Field Ω) (_ : IsAlgClosed Ω) (_ : Algebra k₁ Ω) (_ : Algebra k₂ Ω),
Spec.map ι₁ ≫ T.fromSpecResidueField x = s₁ ∧
Spec.map ι₂ ≫ T.fromSpecResidueField x = s₂ ∧
ι₁ ≫ CommRingCat.ofHom (algebraMap k₁ Ω) = ι₂ ≫ CommRingCat.ofHom (algebraMap k₂ Ω) ∧
Spec.map (CommRingCat.ofHom (algebraMap k₁ Ω)) ≫ s₁ =
Spec.map (CommRingCat.ofHom (algebraMap k₂ Ω)) ≫ s₂