AlgebraicCurve.mem_riemannRochSpace_of_sum_basis_smul_algebraMap_mem_mapDomain
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MemRRSpaceSumBasisSmulAlgebraMap
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.mem_riemannRochSpace_of_sum_basis_smul_algebraMap_mem_mapDomain
(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] [IsAlgClosed K'] [IsCurveOver K F] [IsCurveOver K' F']
(lift : Place K F → Place K' F')
(hlift_ord : ∀ (P : Place K F) (f : F), (lift P).ord (algebraMap F F' f) = P.ord f)
(hlift_inj : Function.Injective lift)
(D : Divisor K F) {ι : Type*} (B : ι → K') (hB : LinearIndependent K B)
(g : ι →₀ F)
(hmem : (∑ j ∈ g.support, algebraMap K' F' (B j) * algebraMap F F' (g j))
∈ LSpace (K := K') (Finsupp.mapDomain lift D)) :
∀ j, g j ∈ LSpace (K := K) D