Module

Place_restrictAlong_inclusion_of_le_of_le.lean

Nyll.AlgebraicCurves.Places.Place_restrictAlong_inclusion_of_le_of_le

3 declarations indexed from sourceView source ↗

Module documentation

Place restrict Along inclusion of le of le

Imports1

Nyll.AlgebraicCurves.Divisors.Correspondences

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

restrictAlong_incl_incl

L33 ↗

AlgebraicCurves.Places.Proofs.Place_restrictAlong_inclusion_of_le_of_le.AlgebraicCurve.Place.ITransportSeam.restrictAlong_incl_incl

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_restrictAlong_inclusion_of_le_of_le
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ITransportSeam
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve

Lean source · statement

theorem restrictAlong_incl_incl {K E : Type*} [Field K] [Field E] [Algebra K E]
    {S T : IntermediateField K E} (h₁ : S ≤ T) (h₂ : T ≤ S)
    (hι₁ : (IntermediateField.inclusion h₁).toRingHom.IsIntegral) (hι₂ :
      (IntermediateField.inclusion h₂).toRingHom.IsIntegral)
    (W : Place K ↥S) :
    (W.restrictAlong (IntermediateField.inclusion h₂) hι₂).restrictAlong
      (IntermediateField.inclusion h₁) hι₁ = W

theorem

ramificationIndexAlong_incl_eq_one

L46 ↗

AlgebraicCurves.Places.Proofs.Place_restrictAlong_inclusion_of_le_of_le.AlgebraicCurve.Place.ITransportSeam.ramificationIndexAlong_incl_eq_one

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_restrictAlong_inclusion_of_le_of_le
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ITransportSeam
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve

Lean source · statement

theorem ramificationIndexAlong_incl_eq_one {K E : Type*} [Field K] [Field E] [Algebra K E]
    {S T : IntermediateField K E} (h₁ : S ≤ T) (h₂ : T ≤ S)
    (hι₁ : (IntermediateField.inclusion h₁).toRingHom.IsIntegral) (hι₂ :
      (IntermediateField.inclusion h₂).toRingHom.IsIntegral)
    (W' : Place K ↥T) : W'.ramificationIndexAlong (IntermediateField.inclusion h₁) = 1

theorem

restrictAlong_inclusion_of_le_of_le

L85 ↗

AlgebraicCurve.Place.restrictAlong_inclusion_of_le_of_le

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_restrictAlong_inclusion_of_le_of_le
open _root_.AlgebraicCurve
open AlgebraicCurve.Place.ITransportSeam in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.restrictAlong_inclusion_of_le_of_le
    {K E : Type*} [Field K] [Field E] [Algebra K E]
    {S T : IntermediateField K E} (hST : S ≤ T) (hTS : T ≤ S)
    (h : (IntermediateField.inclusion hST).toRingHom.IsIntegral)
    (h' : (IntermediateField.inclusion hTS).toRingHom.IsIntegral) :
    (∀ w : Place K T, (w.restrictAlong (IntermediateField.inclusion hST) h).restrictAlong
      (IntermediateField.inclusion hTS) h' = w) ∧
    (∀ v : Place K S, (v.restrictAlong (IntermediateField.inclusion hTS) h').restrictAlong
      (IntermediateField.inclusion hST) h = v) ∧
    (∀ w : Place K T, w.ramificationIndexAlong
      (IntermediateField.inclusion hST : S →ₐ[K] T) = 1) ∧
    (∀ (w : Place K T) (f : S),
      (w.restrictAlong (IntermediateField.inclusion hST : S →ₐ[K] T) h).ord f =
        w.ord (IntermediateField.inclusion hST f))

Module documentation

Place restrict Along inclusion of le of le

Declarations

restrictAlong_incl_incl

ramificationIndexAlong_incl_eq_one

restrictAlong_inclusion_of_le_of_le