NYLL
Module

LSpace_pullbackConstants_eq_span_of_isConstantFieldExtension.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.LSpace_pullbackConstants_eq_span_of_isConstantFieldExtension
34 declarations indexed from sourceView source ↗

Module documentation

LSpace pullback Constants eq span of is Constant Field Extension

Imports7
Imported by2

Declarations

theorem

ord_nonneg_of_mem

L37 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.ord_nonneg_of_mem
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem ord_nonneg_of_mem {f : L} (hf : f ∈ w.toValuationSubring) : 0 ≤ w.ord f
theorem

mem_of_ord_nonneg

L42 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.mem_of_ord_nonneg
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem mem_of_ord_nonneg {f : L} (hf : 0 ≤ w.ord f) : f ∈ w.toValuationSubring
theorem

ord_algebraMap

L51 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.ord_algebraMap
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem ord_algebraMap (a : k) : w.ord (algebraMap k L a) = 0
theorem

exists_ord_eq

L59 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.exists_ord_eq
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem exists_ord_eq (n : ℤ) : ∃ t : L, t ≠ 0 ∧ w.ord t = n
theorem

restrict_restrict

L75 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.restrict_restrict
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
section RestrictRestrict
variable {k L M N : Type*} [Field k] [Field L] [Field M] [Field N]
  [Algebra k L] [Algebra k M] [Algebra k N]
  [Algebra L M] [Algebra M N] [Algebra L N] [IsScalarTower L M N]
  [IsScalarTower k M N] [IsScalarTower k L N] [IsScalarTower k L M]
  [Algebra.IsIntegral M N] [Algebra.IsIntegral L N] [Algebra.IsIntegral L M]
Lean source · statement
theorem restrict_restrict (W : Place k N) : (W.restrict M).restrict L = W.restrict L
theorem

minpoly_algebraMap_eq_map

L90 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.minpoly_algebraMap_eq_map
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
namespace CFE
section
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
Lean source · statement
theorem minpoly_algebraMap_eq_map [FiniteDimensional K K']
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range) (θ : K') :
    minpoly F (algebraMap K' F' θ) = (minpoly K θ).map (algebraMap K F)
theorem

adjoin_gen_eq_top

L122 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.adjoin_gen_eq_top
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
namespace CFE
section
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
omit [FiniteDimensional K K'] [Algebra.IsSeparable K K'] in
Lean source · statement
theorem adjoin_gen_eq_top (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (pb : PowerBasis K K') :
    Algebra.adjoin F {algebraMap K' F' pb.gen} = ⊤
theorem

isIntegral_algebraMap'

L137 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.isIntegral_algebraMap'
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
namespace CFE
section
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
include K in
omit [Algebra.IsSeparable K K'] in
Lean source · statement
theorem isIntegral_algebraMap' (θ : K') : IsIntegral F (algebraMap K' F' θ)
def

pbF

L141 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.pbF
Documentation

The power basis of the function-field extension induced by a constant-field power basis.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
namespace CFE
section
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
Lean source · statement
def pbF (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (pb : PowerBasis K K') : PowerBasis F F'
theorem

pbF_gen

L146 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.pbF_gen
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
namespace CFE
section
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
omit [Algebra.IsSeparable K K'] in
Lean source · statement
theorem pbF_gen (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (pb : PowerBasis K K') : (pbF hgen pb).gen = algebraMap K' F' pb.gen
theorem

pbF_dim

L150 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.pbF_dim
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
namespace CFE
section
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
omit [Algebra.IsSeparable K K'] in
Lean source · statement
theorem pbF_dim (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    (pb : PowerBasis K K') : (pbF hgen pb).dim = pb.dim
theorem

finiteDimensional'

L156 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.finiteDimensional'
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
namespace CFE
section
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
include K in
Lean source · statement
theorem finiteDimensional' (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤) :
    FiniteDimensional F F'
theorem

isSeparable'

L160 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.isSeparable'
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
namespace CFE
section
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
Lean source · statement
theorem isSeparable' (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range) :
    Algebra.IsSeparable F F'
def

bF

L179 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.bF
Documentation

The induced function-field basis reindexed by the dimension of the constant-field power basis.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
namespace CFE
section
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
Lean source · statement
def bF (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    (pb : PowerBasis K K') : Module.Basis (Fin pb.dim) F F'
theorem

bF_apply

L184 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.bF_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
namespace CFE
section
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
omit [Algebra.IsSeparable K K'] in
Lean source · statement
theorem bF_apply (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    (pb : PowerBasis K K') (i : Fin pb.dim) :
    bF hgen hconst pb i = algebraMap K' F' (pb.basis i)
theorem

bF_repr_algebraMap

L191 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.bF_repr_algebraMap
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
namespace CFE
section
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
omit [Algebra.IsSeparable K K'] in
Lean source · statement
theorem bF_repr_algebraMap (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    (pb : PowerBasis K K') (k : K') (i : Fin pb.dim) :
    (bF hgen hconst pb).repr (algebraMap K' F' k) i = algebraMap K F (pb.basis.repr k i)
theorem

trace_algebraMap'

L204 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.trace_algebraMap'
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
namespace CFE
section
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
Lean source · statement
theorem trace_algebraMap' (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range) (k : K') :
    Algebra.trace F F' (algebraMap K' F' k) = algebraMap K F (Algebra.trace K K' k)
theorem

dualBasis_bF_apply

L216 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.dualBasis_bF_apply
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
namespace CFE
section
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
Lean source · statement
theorem dualBasis_bF_apply (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (pb : PowerBasis K K') (j : Fin pb.dim) :
    (Algebra.traceForm F F').dualBasis (traceForm_nondegenerate F F') (bF hgen hconst pb) j =
      algebraMap K' F' ((Algebra.traceForm K K').dualBasis (traceForm_nondegenerate K K')
        pb.basis j)
theorem

mem_integralClosureAt_of_forall_mem

L248 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.mem_integralClosureAt_of_forall_mem
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
open IsDedekindDomain
namespace CFE
section
variable {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
Lean source · statement
theorem mem_integralClosureAt_of_forall_mem (v : Place K F) (x : F')
    (hx : ∀ w : Place K F', w.restrict F = v → x ∈ w.toValuationSubring) :
    x ∈ integralClosure v.toValuationSubring F'
theorem

isScalarTower_valuationSubring

L261 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.isScalarTower_valuationSubring
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
open IsDedekindDomain
namespace CFE
section
variable {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
omit [FiniteDimensional F F'] [Algebra.IsSeparable F F'] in
Lean source · statement
theorem isScalarTower_valuationSubring (v : Place K F) :
    IsScalarTower K v.toValuationSubring F'
theorem

repr_mem_valuationSubring

L278 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.CFE.repr_mem_valuationSubring
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
open IsDedekindDomain
namespace CFE
section
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional K K']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
Lean source · statement
theorem repr_mem_valuationSubring {ι : Type*} [Finite ι] [DecidableEq ι]
    (b : Module.Basis ι F F') (e : ι → K') (hb : ∀ i, b i = algebraMap K' F' (e i))
    (d : ι → K')
    (hd : ∀ j, (Algebra.traceForm F F').dualBasis (traceForm_nondegenerate F F') b j =
      algebraMap K' F' (d j))
    (hrepr : ∀ (k : K') (i : ι), b.repr (algebraMap K' F' k) i ∈ (algebraMap K F).range)
    (v : Place K F) (x : F')
    (hx : ∀ w : Place K F', w.restrict F = v → x ∈ w.toValuationSubring) (i : ι) :
    b.repr x i ∈ v.toValuationSubring
def

layer

L317 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.layer
Documentation

The intermediate field over F generated by the image of the intermediate constant field.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
open IsDedekindDomain
section Layer
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra F F']
variable (F F') in
Lean source · statement
def layer (K₁ : IntermediateField K K') : IntermediateField F F'
theorem

algebraMap_mem_layer

L322 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.algebraMap_mem_layer
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
open IsDedekindDomain
section Layer
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra F F']
variable (F F') in
variable (K₁ : IntermediateField K K')
Lean source · statement
theorem algebraMap_mem_layer (x : K₁) : algebraMap K' F' (x : K') ∈ layer F F' K₁
def

toLayer

L326 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.toLayer
Documentation

The scalar inclusion from the intermediate constant field into its generated layer.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
open IsDedekindDomain
section Layer
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra F F']
variable (F F') in
variable (K₁ : IntermediateField K K')
Lean source · full declaration
def toLayer : K₁ →+* layer F F' K₁ where
  toFun x := ⟨algebraMap K' F' (x : K'), algebraMap_mem_layer K₁ x⟩
  map_one' := Subtype.ext (by simp)
  map_mul' x y := Subtype.ext (by simp)
  map_zero' := Subtype.ext (by simp)
  map_add' x y := Subtype.ext (by simp)
instance

instAlgebraLayer

L333 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.instAlgebraLayer
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
open IsDedekindDomain
section Layer
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra F F']
variable (F F') in
variable (K₁ : IntermediateField K K')
Lean source · statement
instance instAlgebraLayer : Algebra K₁ (layer F F' K₁)
theorem

coe_algebraMap_layer

L337 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.coe_algebraMap_layer
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
open IsDedekindDomain
section Layer
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra F F']
variable (F F') in
variable (K₁ : IntermediateField K K')
Lean source · statement
theorem coe_algebraMap_layer (x : K₁) :
    ((algebraMap K₁ (layer F F' K₁) x : layer F F' K₁) : F') = algebraMap K' F' (x : K')
instance

instIsScalarTowerLayer₁

L343 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.instIsScalarTowerLayer₁
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
open IsDedekindDomain
section Layer
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra F F']
variable (F F') in
variable (K₁ : IntermediateField K K')
variable [Algebra K F'] [IsScalarTower K K' F'] [Algebra K F] [IsScalarTower K F F']
Lean source · statement
instance instIsScalarTowerLayer₁ : IsScalarTower K K₁ (layer F F' K₁)
instance

instIsScalarTowerLayer₂

L350 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.instIsScalarTowerLayer₂
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
open IsDedekindDomain
section Layer
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra F F']
variable (F F') in
variable (K₁ : IntermediateField K K')
variable [Algebra K F'] [IsScalarTower K K' F'] [Algebra K F] [IsScalarTower K F F']
omit [IsScalarTower K K' F'] in
Lean source · statement
instance instIsScalarTowerLayer₂ : IsScalarTower K (layer F F' K₁) F'
theorem

adjoin_range_layer_eq_top

L353 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.adjoin_range_layer_eq_top
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
open IsDedekindDomain
section Layer
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra F F']
variable (F F') in
variable (K₁ : IntermediateField K K')
variable [Algebra K F'] [IsScalarTower K K' F'] [Algebra K F] [IsScalarTower K F F']
Lean source · statement
theorem adjoin_range_layer_eq_top [Algebra.IsAlgebraic K K'] :
    Algebra.adjoin F (Set.range (algebraMap K₁ (layer F F' K₁))) = ⊤
theorem

exists_finsupp_of_adjoin_eq_top

L378 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.exists_finsupp_of_adjoin_eq_top
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
open IsDedekindDomain
section Main
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
Lean source · full declaration
theorem exists_finsupp_of_adjoin_eq_top
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤) (z : F') :
    ∃ l : K' →₀ F, z = l.sum fun c a => algebraMap F F' a * algebraMap K' F' c := by
  have h1 : z ∈ Subalgebra.toSubmodule (Algebra.adjoin F (Set.range (algebraMap K' F'))) := by
    rw [Subalgebra.mem_toSubmodule, hgen]
    trivial
  have h2 : Submonoid.closure (Set.range (algebraMap K' F')) =
      MonoidHom.mrange (algebraMap K' F') := by
    rw [← MonoidHom.coe_mrange, Submonoid.closure_eq]
  rw [Algebra.adjoin_eq_span, h2, MonoidHom.coe_mrange] at h1
  obtain ⟨l, hl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp h1
  refine ⟨l, ?_⟩
  rw [← hl]
  simp only [Algebra.smul_def]
theorem

span_le_lSpace_pullbackConstants

L395 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.span_le_lSpace_pullbackConstants
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
open IsDedekindDomain
section Main
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
variable [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']
Lean source · statement
theorem span_le_lSpace_pullbackConstants (D : Divisor K F) :
    Submodule.span K' (algebraMap F F' '' (LSpace D : Set F)) ≤
      LSpace (Divisor.pullbackConstants K' F' D)
theorem

mem_span_of_mem_lSpace_pullbackConstants

L411 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.mem_span_of_mem_lSpace_pullbackConstants
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
open IsDedekindDomain
section Main
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
variable [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']
variable [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K']
Lean source · statement
theorem mem_span_of_mem_lSpace_pullbackConstants
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    (D : Divisor K F) {z : F'} (hz : z ∈ LSpace (Divisor.pullbackConstants K' F' D)) :
    z ∈ Submodule.span K' (algebraMap F F' '' (LSpace D : Set F))
theorem

lSpace_pullbackConstants_eq_span

L485 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan.P2mConormLSpace.lSpace_pullbackConstants_eq_span
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
namespace P2mConormLSpace
open IsDedekindDomain
section Main
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
variable [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']
variable [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K']
Lean source · statement
theorem lSpace_pullbackConstants_eq_span
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    (D : Divisor K F) :
    LSpace (Divisor.pullbackConstants K' F' D) =
      Submodule.span K' (algebraMap F F' '' (LSpace D : Set F))
theorem

lSpace_pullbackConstants_eq_span_of_isConstantFieldExtension

L499 ↗
AlgebraicCurve.lSpace_pullbackConstants_eq_span_of_isConstantFieldExtension
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpacePullbackConstantsSpan
open AlgebraicCurve Polynomial
open P2mConormLSpace in
Lean source · statement
theorem _root_.AlgebraicCurve.lSpace_pullbackConstants_eq_span_of_isConstantFieldExtension
    {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
    [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K'] [Algebra.IsIntegral F F']
    [AlgebraicCurve.HasPrincipalDivisors K' F']
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    (D : AlgebraicCurve.Divisor K F) :
    AlgebraicCurve.LSpace (AlgebraicCurve.Divisor.pullbackConstants K' F' D) =
      Submodule.span K' (algebraMap F F' '' (AlgebraicCurve.LSpace D : Set F))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.