Module

SemilinearAut_exists_baseAut_eq_of_constantFieldExtension.lean

Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_exists_baseAut_eq_of_constantFieldExtension

2 declarations indexed from sourceView source ↗

Module documentation

Semilinear Aut exists base Aut eq of constant Field Extension

Imports2

Imported by2

theorem

solution

L28 ↗

AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_exists_baseAut_eq_of_constantFieldExtension.solution

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs
namespace SemilinearAut_exists_baseAut_eq_of_constantFieldExtension
open scoped TensorProduct
open AlgebraicCurve in

Lean source · statement

theorem solution
    (K F K' F' : Type*)
    [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
    [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
    [IsAlgClosed K] [CharZero K]
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
      F)) F)
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    (τ : K' ≃ₐ[K] K') :
    ∃ g : SemilinearAut K' F',
      (∀ a : K', SemilinearAut.baseAut g a = τ a) ∧
      ∀ y : F, g • algebraMap F F' y = algebraMap F F' y

theorem

exists_baseAut_eq_of_constantFieldExtension

L112 ↗

AlgebraicCurve.SemilinearAut.exists_baseAut_eq_of_constantFieldExtension

Source context 3 commands