Hopf problem: toric · diagonal quotient 1

Supporting definitions and proofs for this stage of the six-sphere construction.

@[reducible, inline]

abbrev Mathoverflow1973.DiagonalQuotient.BaseSpace (G : Type u_1) (B : Type u_2) [Group G] [MulAction G B] : Type u_2

The orbit-space quotient of a group action on the base.

Equations

• Mathoverflow1973.DiagonalQuotient.BaseSpace G B = MulAction.orbitRel.Quotient G B

def Mathoverflow1973.DiagonalQuotient.baseQuotient (G : Type u_1) (B : Type u_2) [Group G] [MulAction G B] : B → BaseSpace G B

The quotient map from a base to its orbit space.

Equations

• Mathoverflow1973.DiagonalQuotient.baseQuotient G B = Quotient.mk (MulAction.orbitRel G B)