Module

ProfiniteInvariantResidueLift.lean

Nyll.SchemeTheory.RingTheory.Ramification.ProfiniteInvariantResidueLift

8 declarations indexed from sourceView source ↗

Module documentation

Profinite residue lifts by compact intersection

For each open normal subgroup N, take the actual elements of G whose residue equations hold on every N-fixed original coefficient. These sets are closed, nonempty by the finite quotient lift, and directed downward by intersection of open normal subgroups. Compactness supplies a common element. Open point stabilizers then extend its equation to every original coefficient.

All equations live in B/q. No fixed-ring quotient, auxiliary lift functor, additional target algebra, or presumed residue surjectivity is used.

Imports7

Nyll.SchemeTheory.RingTheory.Ramification.FiniteFixedResidueLift
Mathlib.Data.Set.Lattice.Indexed
Mathlib.Topology.Algebra.ClopenNhdofOne
Mathlib.Topology.Algebra.MulAction
Mathlib.Topology.Algebra.OpenSubgroup
Mathlib.Topology.Compactness.Compact
Mathlib.Topology.Order

Imported by2

def

residueLiftSet

L30 ↗

EtaleFundamentalGroups.Inertia.residueLiftSet

Source context 1 command

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

namespace EtaleFundamentalGroups.Inertia

Lean source · statement

def residueLiftSet
    {B G : Type*} [CommRing B] [Group G] [MulSemiringAction G B]
    [TopologicalSpace G] (q : Ideal B) (φ : (B ⧸ q) ≃+* (B ⧸ q))
    (N : OpenNormalSubgroup G) : Set G

theorem

residueEquation_isClosed

L37 ↗

EtaleFundamentalGroups.Inertia.residueEquation_isClosed

Source context 1 command

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

namespace EtaleFundamentalGroups.Inertia

Lean source · statement

theorem residueEquation_isClosed
    {B G : Type*} [CommRing B] [Group G] [MulSemiringAction G B]
    [TopologicalSpace G] [TopologicalSpace B] [DiscreteTopology B] [ContinuousSMul G B]
    (q : Ideal B) (φ : (B ⧸ q) ≃+* (B ⧸ q)) (x : B) :
    IsClosed {g : G | (Ideal.Quotient.mk q).toFun (g • x) =
      φ.toRingHom.toFun ((Ideal.Quotient.mk q).toFun x)}

theorem

residueLiftSet_isClosed

L47 ↗

EtaleFundamentalGroups.Inertia.residueLiftSet_isClosed

Source context 1 command

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

namespace EtaleFundamentalGroups.Inertia

Lean source · statement

theorem residueLiftSet_isClosed
    {B G : Type*} [CommRing B] [Group G] [MulSemiringAction G B]
    [TopologicalSpace G] [TopologicalSpace B] [DiscreteTopology B] [ContinuousSMul G B]
    (q : Ideal B) (φ : (B ⧸ q) ≃+* (B ⧸ q)) (N : OpenNormalSubgroup G) :
    IsClosed (residueLiftSet q φ N)

theorem

residueLiftSet_directed

L56 ↗

EtaleFundamentalGroups.Inertia.residueLiftSet_directed

Source context 1 command

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

namespace EtaleFundamentalGroups.Inertia

Lean source · full declaration

theorem residueLiftSet_directed
    {B G : Type*} [CommRing B] [Group G] [MulSemiringAction G B]
    [TopologicalSpace G] (q : Ideal B) (φ : (B ⧸ q) ≃+* (B ⧸ q)) :
    Directed (fun S T : Set G => T ⊆ S) (residueLiftSet q φ) := by
  intro N M
  refine ⟨N ⊓ M, ?_, ?_⟩
  · intro g hg x hx
    exact hg x (fun n hn => hx n hn.1)
  · intro g hg x hx
    exact hg x (fun n hn => hx n hn.2)

theorem

residueLiftSet_nonempty

L67 ↗

EtaleFundamentalGroups.Inertia.residueLiftSet_nonempty

Source context 1 command

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

namespace EtaleFundamentalGroups.Inertia

Lean source · statement

theorem residueLiftSet_nonempty
    (A : Type*) {B G : Type*} [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    [Algebra.IsInvariant A B G]
    [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G]
    (q : Ideal B) [q.IsPrime] (φ : (B ⧸ q) ≃+* (B ⧸ q))
    (hφ : φ.toRingHom.comp ((Ideal.Quotient.mk q).comp (algebraMap A B)) =
      (Ideal.Quotient.mk q).comp (algebraMap A B))
    (N : OpenNormalSubgroup G) : (residueLiftSet q φ N).Nonempty

theorem

openNormal_nonempty

L80 ↗

EtaleFundamentalGroups.Inertia.openNormal_nonempty

Source context 1 command

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

namespace EtaleFundamentalGroups.Inertia

Lean source · statement

theorem openNormal_nonempty
    (G : Type*) [Group G] [TopologicalSpace G] [CompactSpace G]
    [TotallyDisconnectedSpace G] [IsTopologicalGroup G] :
    Nonempty (OpenNormalSubgroup G)

theorem

exists_openNormal_fixing

L88 ↗

EtaleFundamentalGroups.Inertia.exists_openNormal_fixing

Source context 1 command

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

namespace EtaleFundamentalGroups.Inertia

Lean source · statement

theorem exists_openNormal_fixing
    (G : Type*) {X : Type*} [Group G] [MulAction G X]
    [TopologicalSpace G] [CompactSpace G] [TotallyDisconnectedSpace G]
    [IsTopologicalGroup G] [TopologicalSpace X] [DiscreteTopology X] [ContinuousSMul G X]
    (x : X) :
    ∃ N : OpenNormalSubgroup G, ∀ n ∈ N.toSubgroup, n • x = x

theorem

profiniteInvariant_exists_residue_lift

L100 ↗

EtaleFundamentalGroups.Inertia.profiniteInvariant_exists_residue_lift

Documentation

A profinite invariant action lifts every residue automorphism fixing its original coefficients to one original group element, on all elements.

Source context 1 command

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

namespace EtaleFundamentalGroups.Inertia

Lean source · statement

theorem profiniteInvariant_exists_residue_lift
    (A : Type*) {B G : Type*} [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    [Algebra.IsInvariant A B G]
    [TopologicalSpace G] [CompactSpace G] [TotallyDisconnectedSpace G]
    [IsTopologicalGroup G] [TopologicalSpace B] [DiscreteTopology B] [ContinuousSMul G B]
    (q : Ideal B) [q.IsPrime] (φ : (B ⧸ q) ≃+* (B ⧸ q))
    (hφ : φ.toRingHom.comp ((Ideal.Quotient.mk q).comp (algebraMap A B)) =
      (Ideal.Quotient.mk q).comp (algebraMap A B)) :
    ∃ g : G, ∀ x : B, (Ideal.Quotient.mk q).toFun (g • x) =
      φ.toRingHom.toFun ((Ideal.Quotient.mk q).toFun x)

Module documentation

Profinite residue lifts by compact intersection

Declarations