Topological monoids with open units

We say that a topological monoid M has open units (IsOpenUnits) if Mˣ is open in M and has the subspace topology (i.e. inverse is continuous).

Typical examples include monoids with discrete topology, topological groups (or fields), and rings R equipped with the I-adic topology where I ≤ J(R) (IsOpenUnits.of_isAdic).

A non-example is 𝔸ₖ, because the topology on ideles is not the induced topology from adeles.

This condition is necessary and sufficient for U(R) to be an open subspace of X(R) for all affine scheme X over R and all affine open subscheme U ⊆ X.

class IsOpenUnits (M : Type u_1) [Monoid M] [TopologicalSpace M] : Prop

We say that a topological monoid M has open units if Mˣ is open in M and has the subspace topology (i.e. inverse is continuous).

Typical examples include monoids with discrete topology, topological groups (or fields), and rings R equipped with the I-adic topology where I ≤ J(R).

• isOpenEmbedding_unitsVal : Topology.IsOpenEmbedding Units.val

theorem isOpenUnits_iff (M : Type u_1) [Monoid M] [TopologicalSpace M] : IsOpenUnits M ↔ Topology.IsOpenEmbedding Units.val

@[instance 900]

instance instIsOpenUnitsOfDiscreteTopology (M : Type u_1) [Monoid M] [TopologicalSpace M] [DiscreteTopology M] : IsOpenUnits M

@[instance 900]

instance instIsOpenUnitsOfContinuousInv {M : Type u_1} [Group M] [TopologicalSpace M] [ContinuousInv M] : IsOpenUnits M

@[instance 900]

instance instIsOpenUnitsOfHasContinuousInv₀OfT1Space {M : Type u_1} [GroupWithZero M] [TopologicalSpace M] [HasContinuousInv₀ M] [T1Space M] : IsOpenUnits M

theorem IsOpenUnits.of_isAdic {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] {I : Ideal R} (hR : IsAdic I) (hI : I ≤ ⊥.jacobson) : IsOpenUnits R

If R has the I-adic topology where I is contained in the jacobson radical (e.g. when R is complete or local), then Rˣ is an open subspace of R.