Module

SemilinearAut_existsUnique_monoidHom_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension.lean

Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_existsUnique_monoidHom_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension

2 declarations indexed from sourceView source ↗

Module documentation

Semilinear Aut exists Unique monoid Hom base Aut eq smul algebra Map eq of constant Field

Extension

Imports2

Imported by1

Nyll.AlgebraicCurves.Divisors.Semilinear.All

theorem

solution

L27 ↗

AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearConstantExtension.solution

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearConstantExtension
open AlgebraicCurve

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')) = ⊤)
    (S : Type*) [Group S] (galF : S →* SemilinearAut K F) (τ : S →* (K' ≃+* K'))
    (hτ : ∀ (σ : S) (a : K), τ σ (algebraMap K K' a) = algebraMap K K' (SemilinearAut.baseAut (galF
      σ) a)) :
    ∃! galF' : S →* SemilinearAut K' F',
      (∀ (σ : S) (c : K'), SemilinearAut.baseAut (galF' σ) c = τ σ c) ∧
      ∀ (σ : S) (y : F), galF' σ • algebraMap F F' y = algebraMap F F' (galF σ • y)

theorem

existsUnique_monoidHom_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension

L75 ↗

AlgebraicCurve.SemilinearAut.existsUnique_monoidHom_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension

Source context 2 commands