AlgebraicCurve.CurveModel.exists_curveModel_iso_ffEquiv_symm_germToFunctionField_eq_of_algEquiv
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurve.CurveModel
universe u v
open _root_.AlgebraicCurves.Models.Proofs in
open CurveModel_exists_curveModel_iso_ffEquiv_symm_germToFunctionField_eq_of_algEquiv in
open CategoryTheory AlgebraicGeometry AlgebraicCurve inLean source · statement
theorem exists_curveModel_iso_ffEquiv_symm_germToFunctionField_eq_of_algEquiv
{K : Type u} [Field K] {L L' : Type v} [Field L] [Field L'] [Algebra K L] [Algebra K L']
(e : L ≃ₐ[K] L') (M : AlgebraicCurve.CurveModel K L) :
∃ (M' : AlgebraicCurve.CurveModel K L') (f : M'.C ≅ M.C), f.hom ≫ M.toBase = M'.toBase ∧
∀ (V : M.C.Opens) [Nonempty (Scheme.Opens.toScheme V)] [Nonempty (Scheme.Opens.toScheme
(f.hom ⁻¹ᵁ V))]
(t : Γ(M.C, V)),
M'.ffEquiv.symm (M'.C.germToFunctionField (f.hom ⁻¹ᵁ V) ((f.hom.app V).hom t)) =
e (M.ffEquiv.symm (M.C.germToFunctionField V t))