Covering maps to quotients by free and properly discontinuous group actions

structure IsAddQuotientCoveringMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (G : Type u_4) [AddGroup G] [AddAction G E] extends Topology.IsQuotientMap f, ContinuousConstVAdd G E : Prop

A function from a topological space E with an action by a discrete group to another topological space X is a quotient covering map if it is a quotient map, the action is continuous and transitive on fibers, and every point of E has a neighborhood whose translates by the group elements are pairwise disjoint.

• eq_coinduced : inst✝ = TopologicalSpace.coinduced f inst✝¹
• surjective : Function.Surjective f
• continuous_const_vadd (γ : G) : Continuous fun (x : E) => γ +ᵥ x
• apply_eq_iff_mem_orbit {e₁ e₂ : E} : f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂
• disjoint (e : E) : ∃ U ∈ nhds e, ∀ (g : G), ((fun (x : E) => g +ᵥ x) '' U ∩ U).Nonempty → g = 0

structure IsQuotientCoveringMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (G : Type u_3) [Group G] [MulAction G E] extends Topology.IsQuotientMap f, ContinuousConstSMul G E : Prop

A function from a topological space E with an action by a discrete group to another topological space X is a quotient covering map if it is a quotient map, the action is continuous and transitive on fibers, and every point of E has a neighborhood whose translates by the group elements are pairwise disjoint.

• eq_coinduced : inst✝ = TopologicalSpace.coinduced f inst✝¹
• surjective : Function.Surjective f
• continuous_const_smul (γ : G) : Continuous fun (x : E) => γ • x
• apply_eq_iff_mem_orbit {e₁ e₂ : E} : f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
• disjoint (e : E) : ∃ U ∈ nhds e, ∀ (g : G), ((fun (x : E) => g • x) '' U ∩ U).Nonempty → g = 1

theorem isQuotientCoveringMap_iff {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (G : Type u_3) [Group G] [MulAction G E] : IsQuotientCoveringMap f G ↔ Topology.IsQuotientMap f ∧ ContinuousConstSMul G E ∧ (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) ∧ ∀ (e : E), ∃ U ∈ nhds e, ∀ (g : G), ((fun (x : E) => g • x) '' U ∩ U).Nonempty → g = 1

theorem isAddQuotientCoveringMap_iff {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (G : Type u_3) [AddGroup G] [AddAction G E] : IsAddQuotientCoveringMap f G ↔ Topology.IsQuotientMap f ∧ ContinuousConstVAdd G E ∧ (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) ∧ ∀ (e : E), ∃ U ∈ nhds e, ∀ (g : G), ((fun (x : E) => g +ᵥ x) '' U ∩ U).Nonempty → g = 0

theorem IsQuotientCoveringMap.subgroup_congr {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (G : Type u_3) [Group G] [MulAction G E] (S S' : Subgroup G) (eq : S = S') : IsQuotientCoveringMap f ↥S ↔ IsQuotientCoveringMap f ↥S'

theorem IsAddQuotientCoveringMap.addSubgroup_congr {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (G : Type u_3) [AddGroup G] [AddAction G E] (S S' : AddSubgroup G) (eq : S = S') : IsAddQuotientCoveringMap f ↥S ↔ IsAddQuotientCoveringMap f ↥S'

theorem IsQuotientCoveringMap.map_smul {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) (g : G) {e : E} : f (g • e) = f e

theorem IsAddQuotientCoveringMap.map_vadd {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [AddGroup G] [AddAction G E] (hf : IsAddQuotientCoveringMap f G) (g : G) {e : E} : f (g +ᵥ e) = f e

theorem IsQuotientCoveringMap.isCancelSMul {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) : IsCancelSMul G E

The group action on the domain of a quotient covering map is free.

theorem IsAddQuotientCoveringMap.isCancelVAdd {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [AddGroup G] [AddAction G E] (hf : IsAddQuotientCoveringMap f G) : IsCancelVAdd G E

theorem IsQuotientCoveringMap.homeomorph_comp {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) {Y : Type u_4} [TopologicalSpace Y] (φ : X ≃ₜ Y) : IsQuotientCoveringMap (⇑φ ∘ f) G

theorem IsAddQuotientCoveringMap.homeomorph_comp {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [AddGroup G] [AddAction G E] (hf : IsAddQuotientCoveringMap f G) {Y : Type u_4} [TopologicalSpace Y] (φ : X ≃ₜ Y) : IsAddQuotientCoveringMap (⇑φ ∘ f) G

@[simp]

theorem IsQuotientCoveringMap.homeomorph_comp_iff {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] {Y : Type u_4} [TopologicalSpace Y] (φ : X ≃ₜ Y) : IsQuotientCoveringMap (⇑φ ∘ f) G ↔ IsQuotientCoveringMap f G

@[simp]

theorem IsAddQuotientCoveringMap.homeomorph_comp_iff {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [AddGroup G] [AddAction G E] {Y : Type u_4} [TopologicalSpace Y] (φ : X ≃ₜ Y) : IsAddQuotientCoveringMap (⇑φ ∘ f) G ↔ IsAddQuotientCoveringMap f G

noncomputable def IsQuotientCoveringMap.fiberEquivGroup {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) {x : X} (e : ↑(f ⁻¹' {x})) : ↑(f ⁻¹' {x}) ≃ G

Fibers of a quotient covering map by a group G is a G-torsor.

Equations

• hf.fiberEquivGroup e = (Equiv.ofBijective (fun (g : G) => ⟨g • ↑e, ⋯⟩) ⋯).symm

noncomputable def IsAddQuotientCoveringMap.fiberEquivAddGroup {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [AddGroup G] [AddAction G E] (hf : IsAddQuotientCoveringMap f G) {x : X} (e : ↑(f ⁻¹' {x})) : ↑(f ⁻¹' {x}) ≃ G

Fibers of a quotient covering map by an additive group G is a G-torsor.

Equations

• hf.fiberEquivAddGroup e = (Equiv.ofBijective (fun (g : G) => ⟨g +ᵥ ↑e, ⋯⟩) ⋯).symm

@[simp]

theorem IsQuotientCoveringMap.fiberEquivGroup_self {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) {x : X} (e : ↑(f ⁻¹' {x})) : (hf.fiberEquivGroup e) e = 1

@[simp]

theorem IsQuotientCoveringMap.fiberEquivGroup_eq_iff {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) {x : X} (e e' : ↑(f ⁻¹' {x})) (g : G) : (hf.fiberEquivGroup e) e' = g ↔ ↑e' = g • ↑e

@[simp]

theorem IsQuotientCoveringMap.fiberEquivGroup_smul_self {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) {x : X} (e : ↑(f ⁻¹' {x})) {e' : ↑(f ⁻¹' {x})} : (hf.fiberEquivGroup e) e' • ↑e = ↑e'

@[implicit_reducible]

def IsQuotientCoveringMap.mulActionFiber {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) (x : X) : MulAction G ↑(f ⁻¹' {x})

The action of G restricted to the fiber.

Equations

• hf.mulActionFiber x = { carrier := f ⁻¹' {x}, smul_mem' := ⋯ }.mulAction

@[simp]

theorem IsQuotientCoveringMap.coe_mulActionFiber_smul {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) (x : X) (g : G) (e : ↑(f ⁻¹' {x})) : ↑(g • e) = g • ↑e

theorem IsQuotientCoveringMap.mulActionFiber_isPretransitive {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) (x : X) : MulAction.IsPretransitive G ↑(f ⁻¹' {x})

def IsQuotientCoveringMap.toPermFiber {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) (x : X) : G →* Equiv.Perm ↑(f ⁻¹' {x})

A quotient covering map f induces a permutation action on each fiber.

Equations

• hf.toPermFiber x = MulAction.toPermHom G ↑(f ⁻¹' {x})

@[simp]

theorem IsQuotientCoveringMap.toPermFiber_apply_apply_coe {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) (x : X) (a : G) (x✝ : ↑(f ⁻¹' {x})) : ↑(((hf.toPermFiber x) a) x✝) = a • ↑x✝

@[simp]

theorem IsQuotientCoveringMap.toPermFiber_apply_symm_apply_coe {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) (x : X) (a : G) (x✝ : ↑(f ⁻¹' {x})) : ↑((Equiv.symm ((hf.toPermFiber x) a)) x✝) = a⁻¹ • ↑x✝

theorem IsQuotientCoveringMap.toPermFiber_ext {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) (x : X) (e : ↑(f ⁻¹' {x})) {g g' : G} (eq : ((hf.toPermFiber x) g) e = ((hf.toPermFiber x) g') e) : g = g'

theorem IsQuotientCoveringMap.toPermFiber_injective {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) (x : X) : Function.Injective ⇑(hf.toPermFiber x)

theorem IsQuotientCoveringMap.exists_toPermFiber_eq {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) {x : X} (e e' : ↑(f ⁻¹' {x})) : ∃ (g : G), ((hf.toPermFiber x) g) e = e'

noncomputable def Topology.IsQuotientMap.trivializationOfSMulDisjoint {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientMap f) [ContinuousConstSMul G E] (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) [TopologicalSpace G] [DiscreteTopology G] (U : Set E) (open_U : IsOpen U) (disjoint : ∀ (g : G), ((fun (x : E) => g • x) '' U ∩ U).Nonempty → g = 1) : Bundle.Trivialization G f

If a group G acts on a space E and U is an open subset disjoint from all other G-translates of itself, and p is a quotient map by this action, then p admits a Bundle.Trivialization over the base set p(U).

Equations

• hf.trivializationOfSMulDisjoint hfG U open_U disjoint = IsOpen.trivializationDiscrete (fun (g : G) => (fun (x : E) => g • x) ⁻¹' U) (f '' U) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable def Topology.IsQuotientMap.trivializationOfVAddDisjoint {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [AddGroup G] [AddAction G E] (hf : IsQuotientMap f) [ContinuousConstVAdd G E] (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) [TopologicalSpace G] [DiscreteTopology G] (U : Set E) (open_U : IsOpen U) (disjoint : ∀ (g : G), ((fun (x : E) => g +ᵥ x) '' U ∩ U).Nonempty → g = 0) : Bundle.Trivialization G f

If a group G acts on a space E and U is an open subset disjoint from all other G-translates of itself, and p is a quotient map by this action, then p admits a Bundle.Trivialization over the base set p(U).

Equations

• hf.trivializationOfVAddDisjoint hfG U open_U disjoint = IsOpen.trivializationDiscrete (fun (g : G) => (fun (x : E) => g +ᵥ x) ⁻¹' U) (f '' U) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Topology.IsQuotientMap.trivializationOfVAddDisjoint_baseSet {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [AddGroup G] [AddAction G E] (hf : IsQuotientMap f) [ContinuousConstVAdd G E] (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) [TopologicalSpace G] [DiscreteTopology G] (U : Set E) (open_U : IsOpen U) (disjoint : ∀ (g : G), ((fun (x : E) => g +ᵥ x) '' U ∩ U).Nonempty → g = 0) : (hf.trivializationOfVAddDisjoint hfG U open_U disjoint).baseSet = f '' U

@[simp]

theorem Topology.IsQuotientMap.trivializationOfVAddDisjoint_source {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [AddGroup G] [AddAction G E] (hf : IsQuotientMap f) [ContinuousConstVAdd G E] (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) [TopologicalSpace G] [DiscreteTopology G] (U : Set E) (open_U : IsOpen U) (disjoint : ∀ (g : G), ((fun (x : E) => g +ᵥ x) '' U ∩ U).Nonempty → g = 0) : (hf.trivializationOfVAddDisjoint hfG U open_U disjoint).source = f ⁻¹' f '' U

@[simp]

theorem Topology.IsQuotientMap.trivializationOfSMulDisjoint_baseSet {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientMap f) [ContinuousConstSMul G E] (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) [TopologicalSpace G] [DiscreteTopology G] (U : Set E) (open_U : IsOpen U) (disjoint : ∀ (g : G), ((fun (x : E) => g • x) '' U ∩ U).Nonempty → g = 1) : (hf.trivializationOfSMulDisjoint hfG U open_U disjoint).baseSet = f '' U

@[simp]

theorem Topology.IsQuotientMap.trivializationOfVAddDisjoint_target {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [AddGroup G] [AddAction G E] (hf : IsQuotientMap f) [ContinuousConstVAdd G E] (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) [TopologicalSpace G] [DiscreteTopology G] (U : Set E) (open_U : IsOpen U) (disjoint : ∀ (g : G), ((fun (x : E) => g +ᵥ x) '' U ∩ U).Nonempty → g = 0) : (hf.trivializationOfVAddDisjoint hfG U open_U disjoint).target = (f '' U) ×ˢ Set.univ

@[simp]

theorem Topology.IsQuotientMap.trivializationOfSMulDisjoint_target {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientMap f) [ContinuousConstSMul G E] (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) [TopologicalSpace G] [DiscreteTopology G] (U : Set E) (open_U : IsOpen U) (disjoint : ∀ (g : G), ((fun (x : E) => g • x) '' U ∩ U).Nonempty → g = 1) : (hf.trivializationOfSMulDisjoint hfG U open_U disjoint).target = (f '' U) ×ˢ Set.univ

@[simp]

theorem Topology.IsQuotientMap.trivializationOfSMulDisjoint_source {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientMap f) [ContinuousConstSMul G E] (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) [TopologicalSpace G] [DiscreteTopology G] (U : Set E) (open_U : IsOpen U) (disjoint : ∀ (g : G), ((fun (x : E) => g • x) '' U ∩ U).Nonempty → g = 1) : (hf.trivializationOfSMulDisjoint hfG U open_U disjoint).source = f ⁻¹' f '' U

theorem Topology.IsQuotientMap.isCoveringMapOn_of_smul_disjoint {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientMap f) [ContinuousConstSMul G E] (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) (disjoint : ∀ (e : E), ∃ U ∈ nhds e, ∀ (g : G), ((fun (x : E) => g • x) '' U ∩ U).Nonempty → g • e = e) : IsCoveringMapOn f (f '' {e : E | MulAction.stabilizer G e = ⊥})

theorem Topology.IsQuotientMap.isCoveringMapOn_of_vadd_disjoint {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [AddGroup G] [AddAction G E] (hf : IsQuotientMap f) [ContinuousConstVAdd G E] (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) (disjoint : ∀ (e : E), ∃ U ∈ nhds e, ∀ (g : G), ((fun (x : E) => g +ᵥ x) '' U ∩ U).Nonempty → g +ᵥ e = e) : IsCoveringMapOn f (f '' {e : E | AddAction.stabilizer G e = ⊥})

theorem Topology.IsQuotientMap.isCoveringMapOn_of_properlyDiscontinuousSMul {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientMap f) [ContinuousConstSMul G E] (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) [ProperlyDiscontinuousSMul G E] [LocallyCompactSpace E] [T2Space E] : IsCoveringMapOn f (f '' {e : E | MulAction.stabilizer G e = ⊥})

theorem Topology.IsQuotientMap.isCoveringMapOn_of_properlyDiscontinuousVAdd {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [AddGroup G] [AddAction G E] (hf : IsQuotientMap f) [ContinuousConstVAdd G E] (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) [ProperlyDiscontinuousVAdd G E] [LocallyCompactSpace E] [T2Space E] : IsCoveringMapOn f (f '' {e : E | AddAction.stabilizer G e = ⊥})

theorem Topology.IsQuotientMap.isQuotientCoveringMap_of_properlyDiscontinuousSMul {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [Group G] [MulAction G E] (hf : IsQuotientMap f) [ContinuousConstSMul G E] (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) [ProperlyDiscontinuousSMul G E] [LocallyCompactSpace E] [T2Space E] [IsCancelSMul G E] : IsQuotientCoveringMap f G

theorem Topology.IsQuotientMap.isAddQuotientCoveringMap_of_properlyDiscontinuousVAdd {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {G : Type u_3} [AddGroup G] [AddAction G E] (hf : IsQuotientMap f) [ContinuousConstVAdd G E] (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) [ProperlyDiscontinuousVAdd G E] [LocallyCompactSpace E] [T2Space E] [IsCancelVAdd G E] : IsAddQuotientCoveringMap f G

theorem isCoveringMapOn_quotientMk_of_properlyDiscontinuousSMul {E : Type u_1} [TopologicalSpace E] {G : Type u_3} [Group G] [MulAction G E] [ContinuousConstSMul G E] [ProperlyDiscontinuousSMul G E] [LocallyCompactSpace E] [T2Space E] : IsCoveringMapOn (Quotient.mk (MulAction.orbitRel G E)) (Quotient.mk (MulAction.orbitRel G E) '' {e : E | MulAction.stabilizer G e = ⊥})

theorem isCoveringMapOn_quotientMk_of_properlyDiscontinuousVAdd {E : Type u_1} [TopologicalSpace E] {G : Type u_3} [AddGroup G] [AddAction G E] [ContinuousConstVAdd G E] [ProperlyDiscontinuousVAdd G E] [LocallyCompactSpace E] [T2Space E] : IsCoveringMapOn (Quotient.mk (AddAction.orbitRel G E)) (Quotient.mk (AddAction.orbitRel G E) '' {e : E | AddAction.stabilizer G e = ⊥})

theorem isQuotientCoveringMap_quotientMk_of_properlyDiscontinuousSMul {E : Type u_1} [TopologicalSpace E] {G : Type u_3} [Group G] [MulAction G E] [ContinuousConstSMul G E] [ProperlyDiscontinuousSMul G E] [LocallyCompactSpace E] [T2Space E] [IsCancelSMul G E] : IsQuotientCoveringMap (Quotient.mk (MulAction.orbitRel G E)) G

theorem isAddQuotientCoveringMap_quotientMk_of_properlyDiscontinuousVAdd {E : Type u_1} [TopologicalSpace E] {G : Type u_3} [AddGroup G] [AddAction G E] [ContinuousConstVAdd G E] [ProperlyDiscontinuousVAdd G E] [LocallyCompactSpace E] [T2Space E] [IsCancelVAdd G E] : IsAddQuotientCoveringMap (Quotient.mk (AddAction.orbitRel G E)) G

theorem Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroup {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} (hf : IsQuotientMap f) [Group E] [IsTopologicalGroup E] (G : Subgroup E) (hG : IsDiscrete ↑G) (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₂ * e₁⁻¹ ∈ G) : IsQuotientCoveringMap f ↥G

theorem Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroup {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} (hf : IsQuotientMap f) [AddGroup E] [IsTopologicalAddGroup E] (G : AddSubgroup E) (hG : IsDiscrete ↑G) (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₂ + -e₁ ∈ G) : IsAddQuotientCoveringMap f ↥G

theorem Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroupOp {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} (hf : IsQuotientMap f) [Group E] [IsTopologicalGroup E] (G : Subgroup E) (hG : IsDiscrete ↑G) (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁⁻¹ * e₂ ∈ G) : IsQuotientCoveringMap f ↥G.op

theorem Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroupOp {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} (hf : IsQuotientMap f) [AddGroup E] [IsTopologicalAddGroup E] (G : AddSubgroup E) (hG : IsDiscrete ↑G) (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ -e₁ + e₂ ∈ G) : IsAddQuotientCoveringMap f ↥G.op

theorem Topology.IsQuotientMap.isQuotientCoveringMap_of_isDiscrete_ker_monoidHom {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] [Group E] [IsTopologicalGroup E] [Group X] {f : E →* X} (hf : IsQuotientMap ⇑f) (disc : IsDiscrete ↑f.ker) : IsQuotientCoveringMap ⇑f ↥f.ker

theorem Topology.IsQuotientMap.isAddQuotientCoveringMap_of_isDiscrete_ker_addMonoidHom {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] [AddGroup E] [IsTopologicalAddGroup E] [AddGroup X] {f : E →+ X} (hf : IsQuotientMap ⇑f) (disc : IsDiscrete ↑f.ker) : IsAddQuotientCoveringMap ⇑f ↥f.ker

theorem Subgroup.isQuotientCoveringMap {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G) (hS : IsDiscrete ↑S) : IsQuotientCoveringMap QuotientGroup.mk ↥S.op

theorem AddSubgroup.isAddQuotientCoveringMap {G : Type u_4} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (S : AddSubgroup G) (hS : IsDiscrete ↑S) : IsAddQuotientCoveringMap QuotientAddGroup.mk ↥S.op

theorem Subgroup.isQuotientCoveringMap_of_comm {G : Type u_4} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G) (hS : IsDiscrete ↑S) : IsQuotientCoveringMap QuotientGroup.mk ↥S

theorem AddSubgroup.isAddQuotientCoveringMap_of_comm {G : Type u_4} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (S : AddSubgroup G) (hS : IsDiscrete ↑S) : IsAddQuotientCoveringMap QuotientAddGroup.mk ↥S

theorem IsQuotientCoveringMap.isCoveringMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (G : Type u_3) [Group G] [MulAction G E] (h : IsQuotientCoveringMap f G) : IsCoveringMap f

theorem IsAddQuotientCoveringMap.isCoveringMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (G : Type u_3) [AddGroup G] [AddAction G E] (h : IsAddQuotientCoveringMap f G) : IsCoveringMap f

theorem IsQuotientCoveringMap.isOpenQuotientMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (G : Type u_3) [Group G] [MulAction G E] (h : IsQuotientCoveringMap f G) : IsOpenQuotientMap f

theorem IsAddQuotientCoveringMap.isOpenQuotientMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (G : Type u_3) [AddGroup G] [AddAction G E] (h : IsAddQuotientCoveringMap f G) : IsOpenQuotientMap f

theorem isQuotientCoveringMap_iff_isCoveringMap_and {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (G : Type u_3) [Group G] [MulAction G E] : IsQuotientCoveringMap f G ↔ IsCoveringMap f ∧ Function.Surjective f ∧ ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂

theorem isAddQuotientCoveringMap_iff_isCoveringMap_and {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (G : Type u_3) [AddGroup G] [AddAction G E] : IsAddQuotientCoveringMap f G ↔ IsCoveringMap f ∧ Function.Surjective f ∧ ContinuousConstVAdd G E ∧ IsCancelVAdd G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂