Conformal Groupoid

In this file we define the groupoid of conformal maps on normed spaces.

Main definitions

• conformalGroupoid: the groupoid of conformal partial homeomorphisms.

Tags

conformal, groupoid

def conformalPregroupoid {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : Pregroupoid X

The pregroupoid of conformal maps.

Equations

• conformalPregroupoid = { property := fun (f : X → X) (u : Set X) => ∀ x ∈ u, ConformalAt f x, comp := ⋯, id_mem := ⋯, locality := ⋯, congr := ⋯ }

def conformalGroupoid {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : StructureGroupoid X

The groupoid of conformal maps.

Equations

• conformalGroupoid = conformalPregroupoid.groupoid