AlgebraicCurve.Divisor.support_pushforward_subset
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_support_pushforward_subset
open AlgebraicCurve AlgebraicCurve.DivisorLean source · full declaration
theorem _root_.AlgebraicCurve.Divisor.support_pushforward_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'] [DecidableEq (Place K F)] (D : Divisor K F') : (Divisor.pushforward F
D).support ⊆ D.support.image (fun w => w.restrict F) := by
classical
intro v hv
rw [Finsupp.mem_support_iff, pushforward_apply] at hv
obtain ⟨w, hw, hne⟩ := Finset.exists_ne_zero_of_sum_ne_zero hv
refine Finset.mem_image.mpr ⟨w, hw, ?_⟩
by_contra h
exact hne (ite_eq_right h)