Nyll.SchemeTheory.Normalization.SubalgebraNormalizationTowerRamification

theorem

subalgebraNormalizationTowerRingMap_comp_base

SchemeTheory.subalgebraNormalizationTowerRingMap_comp_base

Documentation

The existing literal normalization tower map preserves the original coefficient maps, as follows from its ambient inclusion triangle.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} {L : Type v}
  [CommRing A] [CommRing L] [Algebra A L]

Lean source · statement

theorem subalgebraNormalizationTowerRingMap_comp_base
    (S T : Subalgebra A L) (h : S ≤ T) :
    (subalgebraNormalizationTowerRingMap S T h).comp
        (algebraMap A (subalgebraNormalizationCommAlgCat S)) =
      algebraMap A (subalgebraNormalizationCommAlgCat T)

theorem

subalgebraNormalization_ramificationIdx_tower

L46 ↗

SchemeTheory.subalgebraNormalization_ramificationIdx_tower

Documentation

Ramification indices multiply for the literal normalization inclusion. Its algebra structure is installed from that ring map; its scalar tower, torsion-freeness, and flatness are constructed here from the coefficient triangle and the native injection.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} {L : Type v}
  [CommRing A] [CommRing L] [Algebra A L]

Lean source · full declaration

theorem subalgebraNormalization_ramificationIdx_tower
    (S T : Subalgebra A L) (h : S ≤ T)
    [IsDedekindDomain (subalgebraNormalizationCommAlgCat S)]
    [IsDomain (subalgebraNormalizationCommAlgCat T)]
    (P : Ideal (subalgebraNormalizationCommAlgCat S))
    (Q : Ideal (subalgebraNormalizationCommAlgCat T))
    (hPQ : P = Q.comap (subalgebraNormalizationTowerRingMap S T h)) :
    letI : Algebra (subalgebraNormalizationCommAlgCat S)
        (subalgebraNormalizationCommAlgCat T) :=
      (subalgebraNormalizationTowerRingMap S T h).toAlgebra
    Q.ramificationIdx A = P.ramificationIdx A *
      Q.ramificationIdx (subalgebraNormalizationCommAlgCat S) := by
  let : Algebra (subalgebraNormalizationCommAlgCat S)
      (subalgebraNormalizationCommAlgCat T) :=
    (subalgebraNormalizationTowerRingMap S T h).toAlgebra
  have : IsScalarTower A (subalgebraNormalizationCommAlgCat S)
      (subalgebraNormalizationCommAlgCat T) :=
    IsScalarTower.of_algebraMap_eq'
      (subalgebraNormalizationTowerRingMap_comp_base S T h).symm
  have : Module.IsTorsionFree (subalgebraNormalizationCommAlgCat S)
      (subalgebraNormalizationCommAlgCat T) :=
    (Module.isTorsionFree_iff_algebraMap_injective).mpr
      (subalgebraNormalizationTowerRingMap_injective S T h)
  have : Q.LiesOver P := ⟨hPQ⟩
  exact Ideal.ramificationIdx_tower (R := A) P Q

SubalgebraNormalizationTowerRamification.lean

Module documentation

Ramification indices in normalization towers

subalgebraNormalizationTowerRingMap_comp_base

subalgebraNormalization_ramificationIdx_tower

Module documentation

Ramification indices in normalization towers

Declarations

subalgebraNormalizationTowerRingMap_comp_base

subalgebraNormalization_ramificationIdx_tower