Module

IdealCompositum.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.Inertia.IdealCompositum

2 declarations indexed from sourceView source ↗

Module documentation

Ideal inertia on a compositum

This file combines the ideal-theoretic restriction map with the cyclic group calculation in Abhyankar's lemma. The field-specific construction of the two restriction homomorphisms is deliberately kept separate.

Imports2

Imported by2

theorem

idealInertiaRestriction_prod_injective

L41 ↗

TameAbhyankar.SGA1.idealInertiaRestriction_prod_injective

Documentation

If the two homomorphisms on the ambient acting groups are jointly injective, their restrictions to ideal inertia are jointly injective.

Source context 13 commands

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

noncomputable section
universe uR uL uR' uT uG uL' uR''
namespace TameAbhyankar.SGA1
variable {R : Type uR} {SLeft : Type uL} {SRight : Type uR'} {T : Type uT}
variable [CommRing R] [CommRing SLeft] [CommRing SRight] [CommRing T]
variable [Algebra R SLeft] [Algebra SLeft T] [Algebra R T]
  [IsScalarTower R SLeft T]
variable [Algebra R SRight] [Algebra SRight T]
  [IsScalarTower R SRight T]
variable {G : Type uG} {GLeft : Type uL'} {GRight : Type uR''}
variable [Group G] [Group GLeft] [Group GRight]
variable [MulSemiringAction G T]
  [MulSemiringAction GLeft SLeft] [MulSemiringAction GRight SRight]
variable (resLeft : G →* GLeft) (resRight : G →* GRight)
variable (PLeft : Ideal SLeft) (PRight : Ideal SRight) (Q : Ideal T)
variable [Q.LiesOver PLeft] [Q.LiesOver PRight]

Lean source · statement

theorem idealInertiaRestriction_prod_injective
    (hresLeft : ∀ sigma : G, ∀ x : SLeft,
      algebraMap SLeft T (resLeft sigma • x) = sigma • algebraMap SLeft T x)
    (hresRight : ∀ sigma : G, ∀ x : SRight,
      algebraMap SRight T (resRight sigma • x) = sigma • algebraMap SRight T x)
    (hpair : Function.Injective (resLeft.prod resRight)) :
    Function.Injective
      ((idealInertiaRestriction resLeft PLeft Q hresLeft).prod
        (idealInertiaRestriction resRight PRight Q hresRight))

theorem

idealRelativeInertia_card_eq_one_of_cyclic_of_card_dvd

L68 ↗

TameAbhyankar.SGA1.idealRelativeInertia_card_eq_one_of_cyclic_of_card_dvd