Theorems · Definition · algebraic topology

Topology.IsQuotientMap.trivializationOfSMulDisjoint

{E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {f : E → X} →
          {G : Type u_3} →
            [inst_2 : Group G] →
              [inst_3 : MulAction G E] →
                Topology.IsQuotientMap f →
                  [ContinuousConstSMul G E] →
                    (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) →
                      [inst_5 : TopologicalSpace G] →
                        [DiscreteTopology G] →
                          (U : Set E) →
                            IsOpen U →
                              (∀ (g : G), ((fun x => 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).

Defined in

Mathlib.Topology.Covering.Quotient

Cited by

4 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceGroupMulActionContinuousConstSMulTopologicalSpaceDiscreteTopology