Open subgroups of a topological groups

This files builds the lattice OpenSubgroup G of open subgroups in a topological group G, and its additive version OpenAddSubgroup. This lattice has a top element, the subgroup of all elements, but no bottom element in general. The trivial subgroup which is the natural candidate bottom has no reason to be open (this happens only in discrete groups).

Note that this notion is especially relevant in a non-archimedean context, for instance for p-adic groups.

Main declarations

• OpenSubgroup.isClosed: An open subgroup is automatically closed.
• Subgroup.isOpen_mono: A subgroup containing an open subgroup is open. There are also versions for additive groups, submodules and ideals.
• OpenSubgroup.comap: Open subgroups can be pulled back by a continuous group morphism.

TODO

• Prove that the identity component of a locally path connected group is an open subgroup. Up to now this file is really geared towards non-archimedean algebra, not Lie groups.

structure OpenAddSubgroup (G : Type u_1) [AddGroup G] [TopologicalSpace G] extends AddSubgroup : Type u_1

The type of open subgroups of a topological additive group.

• carrier : Set G
• add_mem' : ∀ {a b : G}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• neg_mem' : ∀ {x : G}, x ∈ self.carrier → -x ∈ self.carrier
• isOpen' : IsOpen self.carrier

structure OpenSubgroup (G : Type u_1) [Group G] [TopologicalSpace G] extends Subgroup : Type u_1

The type of open subgroups of a topological group.

• carrier : Set G
• mul_mem' : ∀ {a b : G}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• inv_mem' : ∀ {x : G}, x ∈ self.carrier → x⁻¹ ∈ self.carrier
• isOpen' : IsOpen self.carrier

instance OpenAddSubgroup.hasCoeAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] : CoeTC (OpenAddSubgroup G) (AddSubgroup G)

Equations

• OpenAddSubgroup.hasCoeAddSubgroup = { coe := OpenAddSubgroup.toAddSubgroup }

instance OpenSubgroup.hasCoeSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] : CoeTC (OpenSubgroup G) (Subgroup G)

Equations

• OpenSubgroup.hasCoeSubgroup = { coe := OpenSubgroup.toSubgroup }

theorem OpenAddSubgroup.toAddSubgroup_injective {G : Type u_1} [AddGroup G] [TopologicalSpace G] : Function.Injective OpenAddSubgroup.toAddSubgroup

abbrev OpenAddSubgroup.toAddSubgroup_injective.match_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] (motive : (x x_1 : OpenAddSubgroup G) → ↑x = ↑x_1 → Prop) : ∀ (x x_1 : OpenAddSubgroup G) (x_2 : ↑x = ↑x_1), (∀ (toSubgroup : AddSubgroup G) (isOpen' isOpen'_1 : IsOpen toSubgroup.carrier), motive { toAddSubgroup := toSubgroup, isOpen' := isOpen' } { toAddSubgroup := toSubgroup, isOpen' := isOpen'_1 } (_ : ↑{ toAddSubgroup := toSubgroup, isOpen' := (_ : IsOpen toSubgroup.carrier) } = ↑{ toAddSubgroup := toSubgroup, isOpen' := (_ : IsOpen toSubgroup.carrier) })) → motive x x_1 x_2

Equations

• (_ : motive x✝¹ x✝ x) = (_ : motive x✝¹ x✝ x)

theorem OpenSubgroup.toSubgroup_injective {G : Type u_1} [Group G] [TopologicalSpace G] : Function.Injective OpenSubgroup.toSubgroup

theorem OpenAddSubgroup.instSetLikeOpenAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] : ∀ (x x_1 : OpenAddSubgroup G), (fun (U : OpenAddSubgroup G) => ↑↑U) x = (fun (U : OpenAddSubgroup G) => ↑↑U) x_1 → x = x_1

instance OpenAddSubgroup.instSetLikeOpenAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] : SetLike (OpenAddSubgroup G) G

Equations

• One or more equations did not get rendered due to their size.

instance OpenSubgroup.instSetLikeOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] : SetLike (OpenSubgroup G) G

Equations

• One or more equations did not get rendered due to their size.

instance OpenAddSubgroup.instAddSubgroupClassOpenAddSubgroupToSubNegAddMonoidInstSetLikeOpenAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] : AddSubgroupClass (OpenAddSubgroup G) G

Equations

• (_ : AddSubgroupClass (OpenAddSubgroup G) G) = (_ : AddSubgroupClass (OpenAddSubgroup G) G)

instance OpenSubgroup.instSubgroupClassOpenSubgroupToDivInvMonoidInstSetLikeOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] : SubgroupClass (OpenSubgroup G) G

Equations

• (_ : SubgroupClass (OpenSubgroup G) G) = (_ : SubgroupClass (OpenSubgroup G) G)

def OpenAddSubgroup.toOpens {G : Type u_1} [AddGroup G] [TopologicalSpace G] (U : OpenAddSubgroup G) : TopologicalSpace.Opens G

Coercion from OpenAddSubgroup G to Opens G.

Equations

• ↑U = { carrier := ↑U, is_open' := (_ : IsOpen U.carrier) }

def OpenSubgroup.toOpens {G : Type u_1} [Group G] [TopologicalSpace G] (U : OpenSubgroup G) : TopologicalSpace.Opens G

Coercion from OpenSubgroup G to Opens G.

Equations

• ↑U = { carrier := ↑U, is_open' := (_ : IsOpen U.carrier) }

instance OpenAddSubgroup.hasCoeOpens {G : Type u_1} [AddGroup G] [TopologicalSpace G] : CoeTC (OpenAddSubgroup G) (TopologicalSpace.Opens G)

Equations

• OpenAddSubgroup.hasCoeOpens = { coe := OpenAddSubgroup.toOpens }

instance OpenSubgroup.hasCoeOpens {G : Type u_1} [Group G] [TopologicalSpace G] : CoeTC (OpenSubgroup G) (TopologicalSpace.Opens G)

Equations

• OpenSubgroup.hasCoeOpens = { coe := OpenSubgroup.toOpens }

@[simp]

theorem OpenAddSubgroup.coe_toOpens {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} : ↑↑U = ↑U

@[simp]

theorem OpenSubgroup.coe_toOpens {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} : ↑↑U = ↑U

@[simp]

theorem OpenAddSubgroup.coe_toAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} : ↑↑U = ↑U

@[simp]

theorem OpenSubgroup.coe_toSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} : ↑↑U = ↑U

@[simp]

theorem OpenAddSubgroup.mem_toOpens {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {g : G} : g ∈ ↑U ↔ g ∈ U

@[simp]

theorem OpenSubgroup.mem_toOpens {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {g : G} : g ∈ ↑U ↔ g ∈ U

@[simp]

theorem OpenAddSubgroup.mem_toAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {g : G} : g ∈ ↑U ↔ g ∈ U

@[simp]

theorem OpenSubgroup.mem_toSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {g : G} : g ∈ ↑U ↔ g ∈ U

theorem OpenAddSubgroup.ext {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {V : OpenAddSubgroup G} (h : ∀ (x : G), x ∈ U ↔ x ∈ V) : U = V

theorem OpenSubgroup.ext {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {V : OpenSubgroup G} (h : ∀ (x : G), x ∈ U ↔ x ∈ V) : U = V

theorem OpenAddSubgroup.isOpen {G : Type u_1} [AddGroup G] [TopologicalSpace G] (U : OpenAddSubgroup G) : IsOpen ↑U

theorem OpenSubgroup.isOpen {G : Type u_1} [Group G] [TopologicalSpace G] (U : OpenSubgroup G) : IsOpen ↑U

theorem OpenAddSubgroup.mem_nhds_zero {G : Type u_1} [AddGroup G] [TopologicalSpace G] (U : OpenAddSubgroup G) : ↑U ∈ nhds 0

theorem OpenSubgroup.mem_nhds_one {G : Type u_1} [Group G] [TopologicalSpace G] (U : OpenSubgroup G) : ↑U ∈ nhds 1

instance OpenAddSubgroup.instTopOpenAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] : Top (OpenAddSubgroup G)

Equations

• OpenAddSubgroup.instTopOpenAddSubgroup = { top := { toAddSubgroup := ⊤, isOpen' := (_ : IsOpen Set.univ) } }

instance OpenSubgroup.instTopOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] : Top (OpenSubgroup G)

Equations

• OpenSubgroup.instTopOpenSubgroup = { top := { toSubgroup := ⊤, isOpen' := (_ : IsOpen Set.univ) } }

@[simp]

theorem OpenAddSubgroup.mem_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] (x : G) : x ∈ ⊤

@[simp]

theorem OpenSubgroup.mem_top {G : Type u_1} [Group G] [TopologicalSpace G] (x : G) : x ∈ ⊤

@[simp]

theorem OpenAddSubgroup.coe_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] : ↑⊤ = Set.univ

@[simp]

theorem OpenSubgroup.coe_top {G : Type u_1} [Group G] [TopologicalSpace G] : ↑⊤ = Set.univ

@[simp]

theorem OpenAddSubgroup.toAddSubgroup_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] : ↑⊤ = ⊤

@[simp]

theorem OpenSubgroup.toSubgroup_top {G : Type u_1} [Group G] [TopologicalSpace G] : ↑⊤ = ⊤

@[simp]

theorem OpenAddSubgroup.toOpens_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] : ↑⊤ = ⊤

@[simp]

theorem OpenSubgroup.toOpens_top {G : Type u_1} [Group G] [TopologicalSpace G] : ↑⊤ = ⊤

instance OpenAddSubgroup.instInhabitedOpenAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] : Inhabited (OpenAddSubgroup G)

Equations

• OpenAddSubgroup.instInhabitedOpenAddSubgroup = { default := ⊤ }

instance OpenSubgroup.instInhabitedOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] : Inhabited (OpenSubgroup G)

Equations

• OpenSubgroup.instInhabitedOpenSubgroup = { default := ⊤ }

theorem OpenAddSubgroup.isClosed {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (U : OpenAddSubgroup G) : IsClosed ↑U

theorem OpenSubgroup.isClosed {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : OpenSubgroup G) : IsClosed ↑U

theorem OpenAddSubgroup.isClopen {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (U : OpenAddSubgroup G) : IsClopen ↑U

theorem OpenSubgroup.isClopen {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : OpenSubgroup G) : IsClopen ↑U

def OpenAddSubgroup.sum {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] (U : OpenAddSubgroup G) (V : OpenAddSubgroup H) : OpenAddSubgroup (G × H)

The product of two open subgroups as an open subgroup of the product group.

Equations

• OpenAddSubgroup.sum U V = { toAddSubgroup := AddSubgroup.prod ↑U ↑V, isOpen' := (_ : IsOpen (↑U ×ˢ ↑V.toAddSubmonoid)) }

theorem OpenAddSubgroup.sum.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] (U : OpenAddSubgroup G) (V : OpenAddSubgroup H) : IsOpen (↑U ×ˢ ↑V.toAddSubmonoid)

def OpenSubgroup.prod {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] (U : OpenSubgroup G) (V : OpenSubgroup H) : OpenSubgroup (G × H)

The product of two open subgroups as an open subgroup of the product group.

Equations

• OpenSubgroup.prod U V = { toSubgroup := Subgroup.prod ↑U ↑V, isOpen' := (_ : IsOpen (↑U ×ˢ ↑V.toSubmonoid)) }

@[simp]

theorem OpenAddSubgroup.coe_sum {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] (U : OpenAddSubgroup G) (V : OpenAddSubgroup H) : ↑(OpenAddSubgroup.sum U V) = ↑U ×ˢ ↑V

@[simp]

theorem OpenSubgroup.coe_prod {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] (U : OpenSubgroup G) (V : OpenSubgroup H) : ↑(OpenSubgroup.prod U V) = ↑U ×ˢ ↑V

@[simp]

theorem OpenAddSubgroup.toAddSubgroup_sum {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] (U : OpenAddSubgroup G) (V : OpenAddSubgroup H) : ↑(OpenAddSubgroup.sum U V) = AddSubgroup.prod ↑U ↑V

@[simp]

theorem OpenSubgroup.toSubgroup_prod {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] (U : OpenSubgroup G) (V : OpenSubgroup H) : ↑(OpenSubgroup.prod U V) = Subgroup.prod ↑U ↑V

instance OpenAddSubgroup.instInfOpenAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] : Inf (OpenAddSubgroup G)

Equations

• OpenAddSubgroup.instInfOpenAddSubgroup = { inf := fun (U V : OpenAddSubgroup G) => { toAddSubgroup := ↑U ⊓ ↑V, isOpen' := (_ : IsOpen (↑U ∩ ↑V.toAddSubmonoid)) } }

theorem OpenAddSubgroup.instInfOpenAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] (U : OpenAddSubgroup G) (V : OpenAddSubgroup G) : IsOpen (↑U ∩ ↑V.toAddSubmonoid)

instance OpenSubgroup.instInfOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] : Inf (OpenSubgroup G)

Equations

• OpenSubgroup.instInfOpenSubgroup = { inf := fun (U V : OpenSubgroup G) => { toSubgroup := ↑U ⊓ ↑V, isOpen' := (_ : IsOpen (↑U ∩ ↑V.toSubmonoid)) } }

@[simp]

theorem OpenAddSubgroup.coe_inf {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {V : OpenAddSubgroup G} : ↑(U ⊓ V) = ↑U ∩ ↑V

@[simp]

theorem OpenSubgroup.coe_inf {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {V : OpenSubgroup G} : ↑(U ⊓ V) = ↑U ∩ ↑V

@[simp]

theorem OpenAddSubgroup.toAddSubgroup_inf {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {V : OpenAddSubgroup G} : ↑(U ⊓ V) = ↑U ⊓ ↑V

@[simp]

theorem OpenSubgroup.toSubgroup_inf {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {V : OpenSubgroup G} : ↑(U ⊓ V) = ↑U ⊓ ↑V

@[simp]

theorem OpenAddSubgroup.toOpens_inf {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {V : OpenAddSubgroup G} : ↑(U ⊓ V) = ↑U ⊓ ↑V

@[simp]

theorem OpenSubgroup.toOpens_inf {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {V : OpenSubgroup G} : ↑(U ⊓ V) = ↑U ⊓ ↑V

@[simp]

theorem OpenAddSubgroup.mem_inf {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {V : OpenAddSubgroup G} {x : G} : x ∈ U ⊓ V ↔ x ∈ U ∧ x ∈ V

@[simp]

theorem OpenSubgroup.mem_inf {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {V : OpenSubgroup G} {x : G} : x ∈ U ⊓ V ↔ x ∈ U ∧ x ∈ V

instance OpenAddSubgroup.instPartialOrderOpenAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] : PartialOrder (OpenAddSubgroup G)

Equations

• OpenAddSubgroup.instPartialOrderOpenAddSubgroup = inferInstance

instance OpenSubgroup.instPartialOrderOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] : PartialOrder (OpenSubgroup G)

Equations

• OpenSubgroup.instPartialOrderOpenSubgroup = inferInstance

instance OpenAddSubgroup.instSemilatticeInfOpenAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] : SemilatticeInf (OpenAddSubgroup G)

Equations

• One or more equations did not get rendered due to their size.

theorem OpenAddSubgroup.instSemilatticeInfOpenAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] : Function.Injective SetLike.coe

theorem OpenAddSubgroup.instSemilatticeInfOpenAddSubgroup.proof_4 {G : Type u_1} [AddGroup G] [TopologicalSpace G] (a : OpenAddSubgroup G) (b : OpenAddSubgroup G) : a ⊓ b ≤ b

theorem OpenAddSubgroup.instSemilatticeInfOpenAddSubgroup.proof_3 {G : Type u_1} [AddGroup G] [TopologicalSpace G] (a : OpenAddSubgroup G) (b : OpenAddSubgroup G) : a ⊓ b ≤ a

theorem OpenAddSubgroup.instSemilatticeInfOpenAddSubgroup.proof_5 {G : Type u_1} [AddGroup G] [TopologicalSpace G] (a : OpenAddSubgroup G) (b : OpenAddSubgroup G) (c : OpenAddSubgroup G) : a ≤ b → a ≤ c → a ≤ b ⊓ c

theorem OpenAddSubgroup.instSemilatticeInfOpenAddSubgroup.proof_2 {G : Type u_1} [AddGroup G] [TopologicalSpace G] : ∀ (x x_1 : OpenAddSubgroup G), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

instance OpenSubgroup.instSemilatticeInfOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] : SemilatticeInf (OpenSubgroup G)

Equations

• One or more equations did not get rendered due to their size.

theorem OpenAddSubgroup.instOrderTopOpenAddSubgroupToLEToPreorderInstPartialOrderOpenAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] : ∀ (x : OpenAddSubgroup G), ↑x ⊆ Set.univ

instance OpenAddSubgroup.instOrderTopOpenAddSubgroupToLEToPreorderInstPartialOrderOpenAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] : OrderTop (OpenAddSubgroup G)

Equations

• OpenAddSubgroup.instOrderTopOpenAddSubgroupToLEToPreorderInstPartialOrderOpenAddSubgroup = OrderTop.mk (_ : ∀ (x : OpenAddSubgroup G), ↑x ⊆ Set.univ)

instance OpenSubgroup.instOrderTopOpenSubgroupToLEToPreorderInstPartialOrderOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] : OrderTop (OpenSubgroup G)

Equations

• OpenSubgroup.instOrderTopOpenSubgroupToLEToPreorderInstPartialOrderOpenSubgroup = OrderTop.mk (_ : ∀ (x : OpenSubgroup G), ↑x ⊆ Set.univ)

@[simp]

theorem OpenAddSubgroup.toAddSubgroup_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {V : OpenAddSubgroup G} : ↑U ≤ ↑V ↔ U ≤ V

@[simp]

theorem OpenSubgroup.toSubgroup_le {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {V : OpenSubgroup G} : ↑U ≤ ↑V ↔ U ≤ V

def OpenAddSubgroup.comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] (f : G →+ N) (hf : Continuous ⇑f) (H : OpenAddSubgroup N) : OpenAddSubgroup G

The preimage of an OpenAddSubgroup along a continuous AddMonoid homomorphism is an OpenAddSubgroup.

Equations

• OpenAddSubgroup.comap f hf H = { toAddSubgroup := AddSubgroup.comap f ↑H, isOpen' := (_ : IsOpen (⇑f ⁻¹' ↑H)) }

theorem OpenAddSubgroup.comap.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] (f : G →+ N) (hf : Continuous ⇑f) (H : OpenAddSubgroup N) : IsOpen (⇑f ⁻¹' ↑H)

def OpenSubgroup.comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] (f : G →* N) (hf : Continuous ⇑f) (H : OpenSubgroup N) : OpenSubgroup G

The preimage of an OpenSubgroup along a continuous Monoid homomorphism is an OpenSubgroup.

Equations

• OpenSubgroup.comap f hf H = { toSubgroup := Subgroup.comap f ↑H, isOpen' := (_ : IsOpen (⇑f ⁻¹' ↑H)) }

@[simp]

theorem OpenAddSubgroup.coe_comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] (H : OpenAddSubgroup N) (f : G →+ N) (hf : Continuous ⇑f) : ↑(OpenAddSubgroup.comap f hf H) = ⇑f ⁻¹' ↑H

@[simp]

theorem OpenSubgroup.coe_comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] (H : OpenSubgroup N) (f : G →* N) (hf : Continuous ⇑f) : ↑(OpenSubgroup.comap f hf H) = ⇑f ⁻¹' ↑H

@[simp]

theorem OpenAddSubgroup.toAddSubgroup_comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] (H : OpenAddSubgroup N) (f : G →+ N) (hf : Continuous ⇑f) : ↑(OpenAddSubgroup.comap f hf H) = AddSubgroup.comap f ↑H

@[simp]

theorem OpenSubgroup.toSubgroup_comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] (H : OpenSubgroup N) (f : G →* N) (hf : Continuous ⇑f) : ↑(OpenSubgroup.comap f hf H) = Subgroup.comap f ↑H

@[simp]

theorem OpenAddSubgroup.mem_comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] {H : OpenAddSubgroup N} {f : G →+ N} {hf : Continuous ⇑f} {x : G} : x ∈ OpenAddSubgroup.comap f hf H ↔ f x ∈ H

@[simp]

theorem OpenSubgroup.mem_comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] {H : OpenSubgroup N} {f : G →* N} {hf : Continuous ⇑f} {x : G} : x ∈ OpenSubgroup.comap f hf H ↔ f x ∈ H

theorem OpenAddSubgroup.comap_comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] {P : Type u_3} [AddGroup P] [TopologicalSpace P] (K : OpenAddSubgroup P) (f₂ : N →+ P) (hf₂ : Continuous ⇑f₂) (f₁ : G →+ N) (hf₁ : Continuous ⇑f₁) : OpenAddSubgroup.comap f₁ hf₁ (OpenAddSubgroup.comap f₂ hf₂ K) = OpenAddSubgroup.comap (AddMonoidHom.comp f₂ f₁) (_ : Continuous (⇑f₂ ∘ fun (x : G) => f₁ x)) K

theorem OpenSubgroup.comap_comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] {P : Type u_3} [Group P] [TopologicalSpace P] (K : OpenSubgroup P) (f₂ : N →* P) (hf₂ : Continuous ⇑f₂) (f₁ : G →* N) (hf₁ : Continuous ⇑f₁) : OpenSubgroup.comap f₁ hf₁ (OpenSubgroup.comap f₂ hf₂ K) = OpenSubgroup.comap (MonoidHom.comp f₂ f₁) (_ : Continuous (⇑f₂ ∘ fun (x : G) => f₁ x)) K

theorem AddSubgroup.isOpen_of_mem_nhds {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (H : AddSubgroup G) {g : G} (hg : ↑H ∈ nhds g) : IsOpen ↑H

theorem Subgroup.isOpen_of_mem_nhds {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (H : Subgroup G) {g : G} (hg : ↑H ∈ nhds g) : IsOpen ↑H

theorem AddSubgroup.isOpen_mono {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] {H₁ : AddSubgroup G} {H₂ : AddSubgroup G} (h : H₁ ≤ H₂) (h₁ : IsOpen ↑H₁) : IsOpen ↑H₂

theorem Subgroup.isOpen_mono {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] {H₁ : Subgroup G} {H₂ : Subgroup G} (h : H₁ ≤ H₂) (h₁ : IsOpen ↑H₁) : IsOpen ↑H₂

theorem AddSubgroup.isOpen_of_openAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (H : AddSubgroup G) {U : OpenAddSubgroup G} (h : ↑U ≤ H) : IsOpen ↑H

theorem Subgroup.isOpen_of_openSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (H : Subgroup G) {U : OpenSubgroup G} (h : ↑U ≤ H) : IsOpen ↑H

theorem AddSubgroup.isOpen_of_zero_mem_interior {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (H : AddSubgroup G) (h_1_int : 0 ∈ interior ↑H) : IsOpen ↑H

If a subgroup of an additive topological group has 0 in its interior, then it is open.

theorem Subgroup.isOpen_of_one_mem_interior {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (H : Subgroup G) (h_1_int : 1 ∈ interior ↑H) : IsOpen ↑H

If a subgroup of a topological group has 1 in its interior, then it is open.

theorem OpenAddSubgroup.instSupOpenAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (U : OpenAddSubgroup G) (V : OpenAddSubgroup G) : IsOpen ↑(↑U ⊔ ↑V)

instance OpenAddSubgroup.instSupOpenAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] : Sup (OpenAddSubgroup G)

Equations

• OpenAddSubgroup.instSupOpenAddSubgroup = { sup := fun (U V : OpenAddSubgroup G) => { toAddSubgroup := ↑U ⊔ ↑V, isOpen' := (_ : IsOpen ↑(↑U ⊔ ↑V)) } }

instance OpenSubgroup.instSupOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] : Sup (OpenSubgroup G)

Equations

• OpenSubgroup.instSupOpenSubgroup = { sup := fun (U V : OpenSubgroup G) => { toSubgroup := ↑U ⊔ ↑V, isOpen' := (_ : IsOpen ↑(↑U ⊔ ↑V)) } }

@[simp]

theorem OpenAddSubgroup.toAddSubgroup_sup {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (U : OpenAddSubgroup G) (V : OpenAddSubgroup G) : ↑(U ⊔ V) = ↑U ⊔ ↑V

@[simp]

theorem OpenSubgroup.toSubgroup_sup {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : OpenSubgroup G) (V : OpenSubgroup G) : ↑(U ⊔ V) = ↑U ⊔ ↑V

theorem OpenAddSubgroup.instLatticeOpenAddSubgroup.proof_6 {G : Type u_1} [AddGroup G] [TopologicalSpace G] (a : OpenAddSubgroup G) (b : OpenAddSubgroup G) : a ⊓ b ≤ b

theorem OpenAddSubgroup.instLatticeOpenAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] : ∀ (x x_1 : OpenAddSubgroup G), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

instance OpenAddSubgroup.instLatticeOpenAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] : Lattice (OpenAddSubgroup G)

Equations

• One or more equations did not get rendered due to their size.

theorem OpenAddSubgroup.instLatticeOpenAddSubgroup.proof_5 {G : Type u_1} [AddGroup G] [TopologicalSpace G] (a : OpenAddSubgroup G) (b : OpenAddSubgroup G) : a ⊓ b ≤ a

theorem OpenAddSubgroup.instLatticeOpenAddSubgroup.proof_7 {G : Type u_1} [AddGroup G] [TopologicalSpace G] (a : OpenAddSubgroup G) (b : OpenAddSubgroup G) (c : OpenAddSubgroup G) : a ≤ b → a ≤ c → a ≤ b ⊓ c

theorem OpenAddSubgroup.instLatticeOpenAddSubgroup.proof_4 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (a : OpenAddSubgroup G) (b : OpenAddSubgroup G) (c : OpenAddSubgroup G) : a ≤ c → b ≤ c → a ⊔ b ≤ c

theorem OpenAddSubgroup.instLatticeOpenAddSubgroup.proof_3 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (a : OpenAddSubgroup G) (b : OpenAddSubgroup G) : b ≤ a ⊔ b

theorem OpenAddSubgroup.instLatticeOpenAddSubgroup.proof_2 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (a : OpenAddSubgroup G) (b : OpenAddSubgroup G) : a ≤ a ⊔ b

instance OpenSubgroup.instLatticeOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] : Lattice (OpenSubgroup G)

Equations

• One or more equations did not get rendered due to their size.

theorem Submodule.isOpen_mono {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [TopologicalSpace M] [TopologicalAddGroup M] [Module R M] {U : Submodule R M} {P : Submodule R M} (h : U ≤ P) (hU : IsOpen ↑U) : IsOpen ↑P

theorem Ideal.isOpen_of_isOpen_subideal {R : Type u_1} [CommRing R] [TopologicalSpace R] [TopologicalRing R] {U : Ideal R} {I : Ideal R} (h : U ≤ I) (hU : IsOpen ↑U) : IsOpen ↑I