AlgebraicCurve.Pic0.correspondence_correspondence_comm
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_correspondence_correspondence_comm
open IsDedekindDomain AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Pic0.correspondence_correspondence_comm {K F F₁ F₂ : Type*} [Field K]
[Field F] [Field F₁] [Field F₂] [Algebra K F] [Algebra K F₁] [Algebra K F₂]
[HasPrincipalDivisors K F₁] [HasPrincipalDivisors K F₂] (φ ψ : F →ₐ[K] F₁) (φ' ψ' : F →ₐ[K] F₂)
(hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral) (hφ' : φ'.toRingHom.IsIntegral)
(hψ' : ψ'.toRingHom.IsIntegral) (hFI : FundamentalIdentityAlong K φ hφ) (hfin : FiniteAlong K ψ)
(hN : NormFormulaAlong K ψ hfin) (hFI' : FundamentalIdentityAlong K φ' hφ')
(hfin' : FiniteAlong K ψ') (hN' : NormFormulaAlong K ψ' hfin')
(hcomm : ∀ D : Divisor K F,
Divisor.correspondence φ ψ hφ hψ (Divisor.correspondence φ' ψ' hφ' hψ' D) =
Divisor.correspondence φ' ψ' hφ' hψ' (Divisor.correspondence φ ψ hφ hψ D))
(x : Pic0 K F) :
Pic0.correspondence φ ψ hφ hψ hFI hfin hN
(Pic0.correspondence φ' ψ' hφ' hψ' hFI' hfin' hN' x) =
Pic0.correspondence φ' ψ' hφ' hψ' hFI' hfin' hN'
(Pic0.correspondence φ ψ hφ hψ hFI hfin hN x)