Module

Divisor_correspondence_comm_of_exchange.lean

Nyll.AlgebraicCurves.Divisors.Divisor_correspondence_comm_of_exchange

2 declarations indexed from sourceView source ↗

Module documentation

Divisor correspondence comm of exchange

Imports5

Imported by1

Nyll.AlgebraicCurves.Divisors.All

theorem

comm_of_exchange

L42 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_correspondence_comm_of_exchange.AL4Sol.comm_of_exchange

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_correspondence_comm_of_exchange
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve
namespace AL4Sol
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [HasPrincipalDivisors K F']

Lean source · statement

theorem comm_of_exchange (φ ψ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hψ :
  ψ.toRingHom.IsIntegral)
    (g : F' →ₐ[K] F') (hg : g.toRingHom.IsIntegral) (hgs : Function.Surjective g)
    (h1 : g.comp φ = ψ) (h2 : g.comp ψ = φ) :
    Divisor.correspondence φ ψ hφ hψ = Divisor.correspondence ψ φ hψ hφ

theorem

correspondence_comm_of_exchange

L58 ↗

AlgebraicCurve.Divisor.correspondence_comm_of_exchange

Source context 5 commands