NYLL
Module

Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.lean

Nyll.AlgebraicCurves.Places.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
18 declarations indexed from sourceView source ↗

Module documentation

Place sum ramification Index mul inertia Deg bifiber

Imports15
Imported by2

Declarations

theorem

inertiaDegAlong_congr

L45 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.BifibreDev.inertiaDegAlong_congr
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
namespace BifibreDev
section AlongBridge
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem inertiaDegAlong_congr {φ φ' : F →ₐ[K] F'} (h : φ = φ') (hφ : φ.toRingHom.IsIntegral)
    (hφ' : φ'.toRingHom.IsIntegral) (w : Place K F') :
    w.inertiaDegAlong φ hφ = w.inertiaDegAlong φ' hφ'
theorem

isIntegral_toAlgHom

L52 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.BifibreDev.isIntegral_toAlgHom
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
namespace BifibreDev
section AlongBridge
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [Algebra F F'] [IsScalarTower K F F']
Lean source · statement
theorem isIntegral_toAlgHom [Algebra.IsIntegral F F'] :
    (IsScalarTower.toAlgHom K F F').toRingHom.IsIntegral
theorem

toAlgHom_comp_toAlgHom

L64 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.BifibreDev.toAlgHom_comp_toAlgHom
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
namespace BifibreDev
section Tower
variable {K F E M : Type*} [Field K] [Field F] [Field E] [Field M]
    [Algebra K F] [Algebra K E] [Algebra K M] [Algebra F E] [Algebra E M] [Algebra F M]
    [IsScalarTower F E M] [IsScalarTower K F E] [IsScalarTower K E M] [IsScalarTower K F M]
Lean source · statement
theorem toAlgHom_comp_toAlgHom :
    (IsScalarTower.toAlgHom K E M).comp (IsScalarTower.toAlgHom K F E) =
      IsScalarTower.toAlgHom K F M
theorem

restrict_restrict

L69 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.BifibreDev.restrict_restrict
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
namespace BifibreDev
section Tower
variable {K F E M : Type*} [Field K] [Field F] [Field E] [Field M]
    [Algebra K F] [Algebra K E] [Algebra K M] [Algebra F E] [Algebra E M] [Algebra F M]
    [IsScalarTower F E M] [IsScalarTower K F E] [IsScalarTower K E M] [IsScalarTower K F M]
Lean source · statement
theorem restrict_restrict [Algebra.IsIntegral F E] [Algebra.IsIntegral E M]
    [Algebra.IsIntegral F M] (W : Place K M) : (W.restrict E).restrict F = W.restrict F
theorem

ramificationIndex_eq_mul_ramificationIndex_restrict

L91 ↗
AlgebraicCurve.Place.ramificationIndex_eq_mul_ramificationIndex_restrict
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
section TowerRows
variable {K F E M : Type*} [Field K] [Field F] [Field E] [Field M]
    [Algebra K F] [Algebra K E] [Algebra K M] [Algebra F E] [Algebra E M] [Algebra F M]
    [IsScalarTower F E M] [IsScalarTower K F E] [IsScalarTower K E M] [IsScalarTower K F M]
open scoped _root_.AlgebraicCurve _root_.AlgebraicCurve.Place in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ramificationIndex_eq_mul_ramificationIndex_restrict
    [Algebra.IsIntegral F E] [Algebra.IsIntegral E M] (W : Place K M) :
    W.ramificationIndex F = W.ramificationIndex E * (W.restrict E).ramificationIndex F
theorem

inertiaDeg_eq_mul_inertiaDeg_restrict

L103 ↗
AlgebraicCurve.Place.inertiaDeg_eq_mul_inertiaDeg_restrict
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
section TowerRows
variable {K F E M : Type*} [Field K] [Field F] [Field E] [Field M]
    [Algebra K F] [Algebra K E] [Algebra K M] [Algebra F E] [Algebra E M] [Algebra F M]
    [IsScalarTower F E M] [IsScalarTower K F E] [IsScalarTower K E M] [IsScalarTower K F M]
open scoped _root_.AlgebraicCurve _root_.AlgebraicCurve.Place in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.inertiaDeg_eq_mul_inertiaDeg_restrict
    [Algebra.IsIntegral F E] [Algebra.IsIntegral E M] [Algebra.IsIntegral F M] (W : Place K M) :
    W.inertiaDeg F = W.inertiaDeg E * (W.restrict E).inertiaDeg F
def

resHom

L122 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.BifibreDev.resHom
Documentation

The group homomorphism restricting scalars on field automorphisms.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
namespace BifibreDev
section Action
variable (F M : Type*) [Field F] [Field M] [Algebra F M]
Lean source · full declaration
def resHom (L : Type*) [Field L] [Algebra F L] [Algebra L M] [IsScalarTower F L M] :
    (M ≃ₐ[L] M) →* (M ≃ₐ[F] M) where
  toFun σ := σ.restrictScalars F
  map_one' := AlgEquiv.ext fun _ => rfl
  map_mul' _ _ := AlgEquiv.ext fun _ => rfl
def

galAction

L131 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.BifibreDev.galAction
Documentation

The action of field automorphisms on places obtained through semilinear automorphisms.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
namespace BifibreDev
section Action
variable (F M : Type*) [Field F] [Field M] [Algebra F M]
variable (K : Type*) [Field K] [Algebra K F] [Algebra K M] [IsScalarTower K F M]
Lean source · statement
def galAction : MulAction (M ≃ₐ[F] M) (Place K M)
theorem

gal_smul_def

L139 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.BifibreDev.gal_smul_def
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
namespace BifibreDev
section Action
variable (F M : Type*) [Field F] [Field M] [Algebra F M]
variable (K : Type*) [Field K] [Algebra K F] [Algebra K M] [IsScalarTower K F M]
attribute [local instance] galAction
variable {K F M}
Lean source · statement
theorem gal_smul_def (g : M ≃ₐ[F] M) (W : Place K M) :
    g • W = SemilinearAut.ofAlgAut (g.restrictScalars K) • W
theorem

mem_range_resHom_iff

L144 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.BifibreDev.mem_range_resHom_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
namespace BifibreDev
section Action
variable (F M : Type*) [Field F] [Field M] [Algebra F M]
variable (K : Type*) [Field K] [Algebra K F] [Algebra K M] [IsScalarTower K F M]
attribute [local instance] galAction
variable {K F M}
variable {L : Type*} [Field L] [Algebra F L] [Algebra L M] [IsScalarTower F L M]
Lean source · statement
theorem mem_range_resHom_iff {g : M ≃ₐ[F] M} :
    g ∈ (resHom F M L).range ↔ ∀ x : L, g (algebraMap L M x) = algebraMap L M x
theorem

card_range_resHom

L152 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.BifibreDev.card_range_resHom
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
namespace BifibreDev
section Action
variable (F M : Type*) [Field F] [Field M] [Algebra F M]
variable (K : Type*) [Field K] [Algebra K F] [Algebra K M] [IsScalarTower K F M]
attribute [local instance] galAction
variable {K F M}
variable {L : Type*} [Field L] [Algebra F L] [Algebra L M] [IsScalarTower F L M]
Lean source · statement
theorem card_range_resHom : Nat.card (resHom F M L).range = Nat.card (M ≃ₐ[L] M)
theorem

index_range_resHom

L156 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.BifibreDev.index_range_resHom
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
namespace BifibreDev
section Action
variable (F M : Type*) [Field F] [Field M] [Algebra F M]
variable (K : Type*) [Field K] [Algebra K F] [Algebra K M] [IsScalarTower K F M]
attribute [local instance] galAction
variable {K F M}
variable {L : Type*} [Field L] [Algebra F L] [Algebra L M] [IsScalarTower F L M]
Lean source · statement
theorem index_range_resHom [FiniteDimensional F M] [IsGalois F M] [FiniteDimensional L M]
    [IsGalois L M] : (resHom F M L).range.index = Module.finrank F L
theorem

orbit_range_resHom_eq

L167 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.BifibreDev.orbit_range_resHom_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
namespace BifibreDev
section Action
variable (F M : Type*) [Field F] [Field M] [Algebra F M]
variable (K : Type*) [Field K] [Algebra K F] [Algebra K M] [IsScalarTower K F M]
attribute [local instance] galAction
variable {K F M}
variable {L : Type*} [Field L] [Algebra F L] [Algebra L M] [IsScalarTower F L M]
variable [Algebra K L] [IsScalarTower K L M]
Lean source · statement
theorem orbit_range_resHom_eq [FiniteDimensional L M] [IsGalois L M] (P : Place K M) :
    MulAction.orbit (resHom F M L).range P = ↑((P.restrict L).fiberOver M)
theorem

orbit_gal_eq

L178 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.BifibreDev.orbit_gal_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
namespace BifibreDev
section Action
variable (F M : Type*) [Field F] [Field M] [Algebra F M]
variable (K : Type*) [Field K] [Algebra K F] [Algebra K M] [IsScalarTower K F M]
attribute [local instance] galAction
variable {K F M}
variable {L : Type*} [Field L] [Algebra F L] [Algebra L M] [IsScalarTower F L M]
variable [Algebra K L] [IsScalarTower K L M]
omit [Algebra F L] [Algebra L M] [IsScalarTower F L M] [Algebra K L] [IsScalarTower K L M] in
Lean source · statement
theorem orbit_gal_eq [FiniteDimensional F M] [IsGalois F M] (P : Place K M) :
    MulAction.orbit (M ≃ₐ[F] M) P = ↑((P.restrict F).fiberOver M)
theorem

image_val_orbit

L188 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.BifibreDev.image_val_orbit
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
namespace BifibreDev
section Action
variable (F M : Type*) [Field F] [Field M] [Algebra F M]
variable (K : Type*) [Field K] [Algebra K F] [Algebra K M] [IsScalarTower K F M]
attribute [local instance] galAction
variable {K F M}
variable {L : Type*} [Field L] [Algebra F L] [Algebra L M] [IsScalarTower F L M]
variable [Algebra K L] [IsScalarTower K L M]
omit [Algebra F L] [Algebra L M] [IsScalarTower F L M] [Algebra K L] [IsScalarTower K L M] in
Lean source · statement
theorem image_val_orbit {G X : Type*} [Group G] [MulAction G X] (H : Subgroup G) (a : X)
    (x : MulAction.orbit G a) :
    Subtype.val '' MulAction.orbit H x = MulAction.orbit H (x : X)
theorem

forall_apply_algebraMap_eq_of_adjoin_eq_top

L201 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.BifibreDev.forall_apply_algebraMap_eq_of_adjoin_eq_top
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
namespace BifibreDev
section Compositum
variable {F F₁ F₂ E M : Type*} [Field F] [Field F₁] [Field F₂] [Field E] [Field M]
    [Algebra F E] [Algebra F M] [Algebra F₁ E] [Algebra F₂ E] [Algebra F₁ M] [Algebra F₂ M]
    [Algebra E M] [IsScalarTower F E M] [IsScalarTower F₁ E M] [IsScalarTower F₂ E M]
Lean source · statement
theorem forall_apply_algebraMap_eq_of_adjoin_eq_top
    (hgen : Algebra.adjoin F (Set.range (algebraMap F₁ E) ∪ Set.range (algebraMap F₂ E)) = ⊤)
    (g : M ≃ₐ[F] M) (h₁ : ∀ x : F₁, g (algebraMap F₁ M x) = algebraMap F₁ M x)
    (h₂ : ∀ x : F₂, g (algebraMap F₂ M x) = algebraMap F₂ M x) (z : E) :
    g (algebraMap E M z) = algebraMap E M z
theorem

sum_ramificationIndex_mul_inertiaDeg_bifiber

L225 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber.BifibreDev.AlgebraicCurve.Place.sum_ramificationIndex_mul_inertiaDeg_bifiber
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
namespace BifibreDev
attribute [local instance] galAction
Lean source · statement
theorem AlgebraicCurve.Place.sum_ramificationIndex_mul_inertiaDeg_bifiber
    {K F F₁ F₂ E M : Type*} [Field K] [Field F] [Field F₁] [Field F₂] [Field E] [Field M]
    [Algebra K F] [Algebra K F₁] [Algebra K F₂] [Algebra K E] [Algebra K M]
    [Algebra F F₁] [Algebra F F₂] [Algebra F E] [Algebra F M]
    [Algebra F₁ E] [Algebra F₂ E] [Algebra F₁ M] [Algebra F₂ M] [Algebra E M]
    [IsScalarTower K F F₁] [IsScalarTower K F F₂] [IsScalarTower K F E] [IsScalarTower K F M]
    [IsScalarTower K F₁ E] [IsScalarTower K F₂ E] [IsScalarTower K F₁ M] [IsScalarTower K F₂ M]
    [IsScalarTower K E M]
    [IsScalarTower F F₁ M] [IsScalarTower F F₂ M]
    [IsScalarTower F E M] [IsScalarTower F₁ E M] [IsScalarTower F₂ E M]
    [FiniteDimensional F F₁] [FiniteDimensional F F₂] [FiniteDimensional F E]
    [FiniteDimensional F₁ E] [FiniteDimensional F₂ E]
    [FiniteDimensional F M] [IsGalois F M]
    (hgen : Algebra.adjoin F (Set.range (algebraMap F₁ E) ∪ Set.range (algebraMap F₂ E)) = ⊤)
    (hLD : Module.finrank F E = Module.finrank F F₁ * Module.finrank F F₂)
    (v : Place K F) (w₁ : Place K F₁) (w₂ : Place K F₂)
    (hw₁ : w₁.restrict F = v) (hw₂ : w₂.restrict F = v)
    (T : Finset (Place K E)) (hT : ∀ W, W ∈ T ↔ W.restrict F₁ = w₁ ∧ W.restrict F₂ = w₂) :
    ∑ W ∈ T, W.ramificationIndex F * W.inertiaDeg F =
      (w₁.ramificationIndex F * w₁.inertiaDeg F) * (w₂.ramificationIndex F * w₂.inertiaDeg F)
theorem

sum_ramificationIndex_mul_inertiaDeg_bifiber

L381 ↗
AlgebraicCurve.Place.sum_ramificationIndex_mul_inertiaDeg_bifiber
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.Place.sum_ramificationIndex_mul_inertiaDeg_bifiber {K F F₁ F₂ E :
  Type*} (M : Type*) [Field K] [Field F] [Field F₁] [Field F₂] [Field E] [Field M] [Algebra K F]
  [Algebra K F₁] [Algebra K F₂] [Algebra K E] [Algebra K M] [Algebra F F₁] [Algebra F F₂] [Algebra
  F E] [Algebra F M] [Algebra F₁ E] [Algebra F₂ E] [Algebra F₁ M] [Algebra F₂ M] [Algebra E M]
  [IsScalarTower K F F₁] [IsScalarTower K F F₂] [IsScalarTower K F E] [IsScalarTower K F M]
  [IsScalarTower K F₁ E] [IsScalarTower K F₂ E] [IsScalarTower K F₁ M] [IsScalarTower K F₂ M]
  [IsScalarTower K E M] [IsScalarTower F F₁ M] [IsScalarTower F F₂ M] [IsScalarTower F E M]
  [IsScalarTower F₁ E M] [IsScalarTower F₂ E M] [FiniteDimensional F F₁] [FiniteDimensional F F₂]
  [FiniteDimensional F E] [FiniteDimensional F₁ E] [FiniteDimensional F₂ E] [FiniteDimensional F M]
  [IsGalois F M] (hgen : Algebra.adjoin F (Set.range (algebraMap F₁ E) ∪ Set.range (algebraMap F₂
  E)) = ⊤) (hLD : Module.finrank F E = Module.finrank F F₁ * Module.finrank F F₂) (v : Place K F)
  (w₁ : Place K F₁) (w₂ : Place K F₂) (hw₁ : w₁.restrict F = v) (hw₂ : w₂.restrict F = v) (T :
  Finset (Place K E)) (hT : ∀ W, W ∈ T ↔ W.restrict F₁ = w₁ ∧ W.restrict F₂ = w₂) :
    ∑ W ∈ T, W.ramificationIndex F * W.inertiaDeg F = (w₁.ramificationIndex F * w₁.inertiaDeg F) *
      (w₂.ramificationIndex F * w₂.inertiaDeg F)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.