SchemeTheory.idealInertia_isClosed_of_openFixedSets
Open coefficient stabilizers make the actual ideal inertia closed in the given group topology. No compactness or closedness premise is added.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace SchemeTheory
universe u vLean source · full declaration
theorem idealInertia_isClosed_of_openFixedSets
(B : CommRingCat.{u}) (G : GrpCat.{v}) [TopologicalSpace G.carrier]
[IsTopologicalGroup G.carrier] (a : MulSemiringAction G.carrier B.carrier)
(Q : Ideal B.carrier)
(hopen :
let : MulSemiringAction G.carrier B.carrier := a
∀ b : B.carrier, IsOpen (fun g : G.carrier => g • b = b)) :
let : MulSemiringAction G.carrier B.carrier := a
IsClosed (Q.inertia G.carrier).carrier := by
intro ringAction
let : TopologicalSpace B.carrier := ⊥
have : DiscreteTopology B.carrier := ⟨rfl⟩
have : ContinuousSMul G.carrier B.carrier :=
continuousSMul_iff_stabilizer_isOpen.mpr hopen
have hset : (Q.inertia G.carrier).carrier =
⋂ b : B.carrier, {g : G.carrier | g • b - b ∈ Q} := by
ext g
rw [Set.mem_iInter]
exact Ideal.mem_inertia (I := Q) (G := G.carrier) (σ := g)
rw [hset]
apply isClosed_iInter
intro b
have hcont : Continuous (fun g : G.carrier => g • b) :=
continuous_id.smul continuous_const
exact (isClosed_discrete {c : B.carrier | c - b ∈ Q}).preimage hcont