NYLL
Module

FiniteLevelInertiaImage.lean

Nyll.SchemeTheory.RingTheory.Ramification.FiniteLevelInertiaImage
17 declarations indexed from sourceView source ↗

Module documentation

Finite-level images of inertia in an arbitrary Galois normalization

The canonical action on the actual integral closure is continuous for the Krull topology and the discrete ring topology. The subgroup fixing an actual intermediate field has that field's integral closure as its invariant base. These two facts supply the profinite inertia-image theorem at every finite Galois intermediate field. No equality of inertia images is an input.

Imports18
  • Nyll.SchemeTheory.RingTheory.Ramification.ProfiniteInertiaMap
  • Nyll.SchemeTheory.Normalization.SubalgebraPreimage
  • Mathlib.Algebra.Algebra.Equiv
  • Mathlib.Algebra.Ring.Action.Basic
  • Mathlib.Algebra.Algebra.Subalgebra.Basic
  • Mathlib.FieldTheory.Galois.Basic
  • Mathlib.FieldTheory.Galois.GaloisClosure
  • Mathlib.FieldTheory.Galois.Infinite
  • Mathlib.FieldTheory.Galois.Profinite
  • Mathlib.FieldTheory.KrullTopology
  • Mathlib.FieldTheory.Normal.Basic
  • Mathlib.RingTheory.Ideal.Over
  • Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
  • Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
  • Mathlib.RingTheory.IntegralClosure.IntegralRestrict
  • Mathlib.RingTheory.Invariant.Galois
  • Mathlib.Topology.Algebra.MulAction
  • Mathlib.Topology.Compactness.Compact
Imported by26

Declarations

def

integralClosureRestrictionRingHom

L48 ↗
EtaleFundamentalGroups.Inertia.integralClosureRestrictionRingHom
Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
Lean source · statement
def integralClosureRestrictionRingHom
    (A : Type u) (L : Type v) [CommRing A] [CommRing L] [Algebra A L]
    (f : L →ₐ[A] L) : integralClosure A L →+* integralClosure A L
theorem

integralClosureRestrictionRingHom_comp

L54 ↗
EtaleFundamentalGroups.Inertia.integralClosureRestrictionRingHom_comp
Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
Lean source · statement
theorem integralClosureRestrictionRingHom_comp
    (A : Type u) (L : Type v) [CommRing A] [CommRing L] [Algebra A L]
    (f : L →ₐ[A] L) :
    (integralClosure A L).toSubring.subtype.comp (integralClosureRestrictionRingHom A L f) =
      f.toRingHom.comp (integralClosure A L).toSubring.subtype
def

normalizationCommAlgInclusion

L73 ↗
EtaleFundamentalGroups.Inertia.normalizationCommAlgInclusion
Documentation

The literal normalization inclusion on its existing native algebra object.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
section NativeNormalizationCarrier
open SchemeTheory
Lean source · statement
def normalizationCommAlgInclusion
    (A : Type u) (F : Type w) [CommRing A] [CommRing F] [Algebra A F] :
    normalizationCommAlgCat A F →+* F
def

normalizationCommAlgRestrictionRingHom

L79 ↗
EtaleFundamentalGroups.Inertia.normalizationCommAlgRestrictionRingHom
Documentation

The existing normalization restriction on the identical native carrier.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
section NativeNormalizationCarrier
open SchemeTheory
Lean source · statement
def normalizationCommAlgRestrictionRingHom
    (A : Type u) (F : Type w) [CommRing A] [CommRing F] [Algebra A F]
    (f : F →ₐ[A] F) : normalizationCommAlgCat A F →+* normalizationCommAlgCat A F
theorem

normalizationCommAlgRestrictionRingHom_comp

L85 ↗
EtaleFundamentalGroups.Inertia.normalizationCommAlgRestrictionRingHom_comp
Documentation

The actual restriction square is converted before fraction-field data occur.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
section NativeNormalizationCarrier
open SchemeTheory
Lean source · statement
theorem normalizationCommAlgRestrictionRingHom_comp
    (A : Type u) (F : Type w) [CommRing A] [CommRing F] [Algebra A F]
    (f : F →ₐ[A] F) :
    (normalizationCommAlgInclusion A F).comp (normalizationCommAlgRestrictionRingHom A F f) =
      f.toRingHom.comp (normalizationCommAlgInclusion A F)
theorem

galois_fixedSet_isOpen

L96 ↗
EtaleFundamentalGroups.Inertia.galois_fixedSet_isOpen
Documentation

The native field stabilizer is open, with the field action closed in this field-only scope.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
Lean source · full declaration
theorem galois_fixedSet_isOpen
    (K : Type v) (L : Type w) [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L] (x : L) :
    IsOpen (fun σ : Gal(L/K) => σ.toRingHom.toFun x = x) := by
  change IsOpen (MulAction.stabilizer Gal(L/K) x : Set Gal(L/K))
  exact stabilizer_isOpen_of_isIntegral x
theorem

continuousSMul_of_open_fixedSets

L103 ↗
EtaleFundamentalGroups.Inertia.continuousSMul_of_open_fixedSets
Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
Lean source · full declaration
theorem continuousSMul_of_open_fixedSets
    {G X : Type w} [Group G] [MulAction G X]
    [TopologicalSpace G] [IsTopologicalGroup G]
    [TopologicalSpace X] [DiscreteTopology X]
    (hopen : ∀ x : X, IsOpen (fun g : G => g • x = x)) : ContinuousSMul G X :=
  continuousSMul_iff_stabilizer_isOpen.mpr hopen
instance

normalizationInertiaImageAction

L117 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaImageAction
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
section RawNormalizationAction
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
Lean source · statement
instance normalizationInertiaImageAction [Algebra.IsAlgebraic K L] :
    MulSemiringAction Gal(L/K) (integralClosure A L)
instance

normalizationInertiaImageTower

L121 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaImageTower
Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
section RawNormalizationAction
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
local instance normalizationInertiaImageAction [Algebra.IsAlgebraic K L] :
    MulSemiringAction Gal(L/K) (integralClosure A L) :=
  IsIntegralClosure.MulSemiringAction A K L (integralClosure A L)
Lean source · statement
instance normalizationInertiaImageTower (E : IntermediateField K L) :
    IsScalarTower A E L
theorem

normalizationInertiaImageAction_comp_inclusion

L127 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaImageAction_comp_inclusion
Documentation

The actual normalization Galois action commutes with the literal integral-closure inclusion, as a bundled ring-map equality.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
section RawNormalizationAction
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
local instance normalizationInertiaImageAction [Algebra.IsAlgebraic K L] :
    MulSemiringAction Gal(L/K) (integralClosure A L) :=
  IsIntegralClosure.MulSemiringAction A K L (integralClosure A L)
local instance normalizationInertiaImageTower (E : IntermediateField K L) :
    IsScalarTower A E L :=
  Subalgebra.isScalarTower_mid (S := E.toSubalgebra) (α := A) (β := L)
Lean source · statement
theorem normalizationInertiaImageAction_comp_inclusion [IsGalois K L]
    (σ : Gal(L/K)) :
    σ.toRingHom.comp (integralClosure A L).toSubring.subtype =
      (integralClosure A L).toSubring.subtype.comp
        (MulSemiringAction.toRingHom Gal(L/K) (integralClosure A L) σ)
theorem

normalizationInertiaImageAction_fixed_iff

L137 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaImageAction_fixed_iff
Documentation

Fixedness under the prescribed normalization action is detected by its literal inclusion. The actual RingHom coefficient square proves both directions without opening the normalization-to-field algebra.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
section RawNormalizationAction
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
local instance normalizationInertiaImageAction [Algebra.IsAlgebraic K L] :
    MulSemiringAction Gal(L/K) (integralClosure A L) :=
  IsIntegralClosure.MulSemiringAction A K L (integralClosure A L)
local instance normalizationInertiaImageTower (E : IntermediateField K L) :
    IsScalarTower A E L :=
  Subalgebra.isScalarTower_mid (S := E.toSubalgebra) (α := A) (β := L)
Lean source · statement
theorem normalizationInertiaImageAction_fixed_iff [Algebra.IsAlgebraic K L]
    (σ : Gal(L/K)) (b : integralClosure A L) :
    σ • b = b ↔ σ.toRingHom.toFun (b : L) = (b : L)
theorem

integralClosure_fixedSet_isOpen_krull

L153 ↗
EtaleFundamentalGroups.Inertia.integralClosure_fixedSet_isOpen_krull
Documentation

The actual normalization stabilizer is open before a topology on the normalization carrier is introduced.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
section RawNormalizationAction
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
local instance normalizationInertiaImageAction [Algebra.IsAlgebraic K L] :
    MulSemiringAction Gal(L/K) (integralClosure A L) :=
  IsIntegralClosure.MulSemiringAction A K L (integralClosure A L)
local instance normalizationInertiaImageTower (E : IntermediateField K L) :
    IsScalarTower A E L :=
  Subalgebra.isScalarTower_mid (S := E.toSubalgebra) (α := A) (β := L)
Lean source · full declaration
theorem integralClosure_fixedSet_isOpen_krull [Algebra.IsAlgebraic K L]
    (b : integralClosure A L) : IsOpen (fun σ : Gal(L/K) => σ • b = b) := by
  have heq : (fun σ : Gal(L/K) => σ • b = b) =
      (fun σ : Gal(L/K) => σ.toRingHom.toFun (b : L) = (b : L)) :=
    funext (fun σ => propext (normalizationInertiaImageAction_fixed_iff A K L σ b))
  rw [heq]
  exact galois_fixedSet_isOpen K L (b : L)
theorem

integralClosure_continuousSMul_krull

L163 ↗
EtaleFundamentalGroups.Inertia.integralClosure_continuousSMul_krull
Documentation

The existing prescribed normalization action is continuous for the Krull topology and any discrete topology on the literal integral closure.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
section RawNormalizationAction
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
local instance normalizationInertiaImageAction [Algebra.IsAlgebraic K L] :
    MulSemiringAction Gal(L/K) (integralClosure A L) :=
  IsIntegralClosure.MulSemiringAction A K L (integralClosure A L)
local instance normalizationInertiaImageTower (E : IntermediateField K L) :
    IsScalarTower A E L :=
  Subalgebra.isScalarTower_mid (S := E.toSubalgebra) (α := A) (β := L)
Lean source · statement
theorem integralClosure_continuousSMul_krull [Algebra.IsAlgebraic K L]
    [TopologicalSpace (integralClosure A L)] [DiscreteTopology (integralClosure A L)] :
    ContinuousSMul Gal(L/K) (integralClosure A L)
theorem

integralClosure_isInvariant_fixingSubgroup

L168 ↗
EtaleFundamentalGroups.Inertia.integralClosure_isInvariant_fixingSubgroup
Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
section RawNormalizationAction
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
local instance normalizationInertiaImageAction [Algebra.IsAlgebraic K L] :
    MulSemiringAction Gal(L/K) (integralClosure A L) :=
  IsIntegralClosure.MulSemiringAction A K L (integralClosure A L)
local instance normalizationInertiaImageTower (E : IntermediateField K L) :
    IsScalarTower A E L :=
  Subalgebra.isScalarTower_mid (S := E.toSubalgebra) (α := A) (β := L)
Lean source · full declaration
theorem integralClosure_isInvariant_fixingSubgroup [IsGalois K L]
    (E : IntermediateField K L) :
    let : Algebra (integralClosure A E) (integralClosure A L) :=
      (IsScalarTower.toAlgHom A E L).mapIntegralClosure.toRingHom.toAlgebra
    Algebra.IsInvariant (integralClosure A E) (integralClosure A L) E.fixingSubgroup := by
  intro inclusionAction
  constructor
  intro b hb
  have hbE : (b : L) ∈ E := by
    rw [← InfiniteGalois.fixedField_fixingSubgroup E]
    apply (IntermediateField.mem_fixedField_iff (E.fixingSubgroup) (b : L)).mpr
    intro σ hσ
    have h := hb ⟨σ, hσ⟩
    change galRestrict A K L (integralClosure A L) σ b = b at h
    exact (algebraMap_galRestrict_apply A σ b).symm.trans (congrArg Subtype.val h)
  let e : E := ⟨(b : L), hbE⟩
  have he : IsIntegral A e :=
    (isIntegral_algHom_iff (IsScalarTower.toAlgHom A E L)
      (algebraMap E L).injective).mp b.property
  refine ⟨⟨e, he⟩, ?_⟩
  apply Subtype.ext
  rfl
theorem

integralClosure_inertia_map_eq_finiteGalois_contraction

L195 ↗
EtaleFundamentalGroups.Inertia.integralClosure_inertia_map_eq_finiteGalois_contraction
Documentation

Restricting inertia in an arbitrary Galois normalization to an actual finite Galois intermediate field gives the entire inertia group of the literal contracted prime. The prime is arbitrary, and the ambient extension is not assumed finite.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
section RawNormalizationAction
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
local instance normalizationInertiaImageAction [Algebra.IsAlgebraic K L] :
    MulSemiringAction Gal(L/K) (integralClosure A L) :=
  IsIntegralClosure.MulSemiringAction A K L (integralClosure A L)
local instance normalizationInertiaImageTower (E : IntermediateField K L) :
    IsScalarTower A E L :=
  Subalgebra.isScalarTower_mid (S := E.toSubalgebra) (α := A) (β := L)
Lean source · statement
theorem integralClosure_inertia_map_eq_finiteGalois_contraction [IsGalois K L]
    (E : FiniteGaloisIntermediateField K L)
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] :
    (Q.inertia Gal(L/K)).map (AlgEquiv.restrictNormalHom E) =
      (Q.comap (IsScalarTower.toAlgHom A E L).mapIntegralClosure).inertia Gal(E/K)
abbrev

normalizationCommAlgGaloisAction

L242 ↗
EtaleFundamentalGroups.Inertia.normalizationCommAlgGaloisAction
Documentation

The already prescribed normalization action, on its identical native carrier. This is the existing action value, without a new action construction.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
section NativeNormalizationAction
open SchemeTheory
Lean source · statement
abbrev normalizationCommAlgGaloisAction
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K] [Algebra K F] [Algebra A F]
    [IsScalarTower A K F] [Algebra.IsAlgebraic K F] :
    MulSemiringAction Gal(F/K) (normalizationCommAlgCat A F).carrier
theorem

normalizationCommAlg_action_comp_inclusion

L253 ↗
EtaleFundamentalGroups.Inertia.normalizationCommAlg_action_comp_inclusion
Documentation

The actual action-inclusion square, through the native restriction owner.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The forward map in Mathlib's `galRestrict'` is precisely the following
composition of existing native maps. Keeping its A-linear input in this
sparse scope avoids reopening the entire AKLB scalar interface downstream.
Source: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
-/
section NativeNormalizationAction
open SchemeTheory
attribute [local instance] normalizationCommAlgGaloisAction
Lean source · statement
theorem normalizationCommAlg_action_comp_inclusion
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K] [Algebra K F] [Algebra A F]
    [IsScalarTower A K F] [Algebra.IsAlgebraic K F] (σ : Gal(F/K)) :
    σ.toRingHom.comp (normalizationCommAlgInclusion A F) =
      (normalizationCommAlgInclusion A F).comp
        (MulSemiringAction.toRingHom Gal(F/K) (normalizationCommAlgCat A F) σ)

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