theorem
L26 ↗support_pullback_subset
AlgebraicCurve.Divisor.support_pullback_subset
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_support_pullback_subset
open AlgebraicCurve AlgebraicCurve.DivisorLean source · full declaration
theorem _root_.AlgebraicCurve.Divisor.support_pullback_subset {K F F' : Type*} [Field K] [Field F]
[Field F'] [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral
F F'] [HasPrincipalDivisors K F'] [DecidableEq (Place K F')] (E : Divisor K F) :
(Divisor.pullback F' E).support ⊆ E.support.biUnion (fun v => v.fiber F') := by
classical
intro w hw
exact Finset.mem_biUnion.mpr ⟨w.restrict F,
restrict_mem_support_of_mem_support_pullback hw, w.restrict_mem_fiber⟩