Module

CurveModel_exists_curveModel_iso_of_algEquiv.lean

Nyll.AlgebraicCurves.Models.CurveModel_exists_curveModel_iso_of_algEquiv

1 declaration indexed from sourceView source ↗

Module documentation

Curve Model exists curve Model iso of alg Equiv

Imports2

Imported by4

theorem

exists_curveModel_iso_of_algEquiv

L28 ↗

AlgebraicCurve.CurveModel.exists_curveModel_iso_of_algEquiv

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_iso_of_algEquiv
open CategoryTheory AlgebraicGeometry AlgebraicCurve
universe u v

Lean source · statement

theorem _root_.AlgebraicCurve.CurveModel.exists_curveModel_iso_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

Module documentation

Curve Model exists curve Model iso of alg Equiv

Declarations

exists_curveModel_iso_of_algEquiv