AlgebraicCurve.exists_linearEquiv_cechH1_swap
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.Exists_linearEquiv_cechH1_swap
universe u vLean source · statement
theorem _root_.AlgebraicCurve.exists_linearEquiv_cechH1_swap
{K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
(S S' : Set (AlgebraicCurve.Place K F)) (D : AlgebraicCurve.Divisor K F) :
∃ e : AlgebraicCurve.cechH1 S S' D ≃ₗ[K] AlgebraicCurve.cechH1 S' S D,
∀ (f : F) (h : f ∈ AlgebraicCurve.lSpaceOn (S ∩ S') D) (h' : f ∈ AlgebraicCurve.lSpaceOn (S'
∩ S) D),
e (Submodule.Quotient.mk ⟨f, h⟩) = Submodule.Quotient.mk ⟨f, h'⟩