# Induced and coinduced topologies #

In this file we define the induced and coinduced topologies, as well as topology inducing maps, topological embeddings, and quotient maps.

## Main definitions #

`TopologicalSpace.induced`

: given`f : X → Y`

and a topology on`Y`

, the induced topology on`X`

is the collection of sets that are preimages of some open set in`Y`

. This is the coarsest topology that makes`f`

continuous.`TopologicalSpace.coinduced`

: given`f : X → Y`

and a topology on`X`

, the coinduced topology on`Y`

is defined such that`s : Set Y`

is open if the preimage of`s`

is open. This is the finest topology that makes`f`

continuous.`Inducing`

: a map`f : X → Y`

is called*inducing*, if the topology on the domain is equal to the induced topology.`Embedding`

: a map`f : X → Y`

is an*embedding*, if it is a topology inducing map and it is injective.`OpenEmbedding`

: a map`f : X → Y`

is an*open embedding*, if it is an embedding and its range is open. An open embedding is an open map.`ClosedEmbedding`

: a map`f : X → Y`

is an*open embedding*, if it is an embedding and its range is open. An open embedding is an open map.`QuotientMap`

: a map`f : X → Y`

is a*quotient map*, if it is surjective and the topology on the codomain is equal to the coinduced topology.

Given `f : X → Y`

and a topology on `Y`

,
the induced topology on `X`

is the collection of sets
that are preimages of some open set in `Y`

.
This is the coarsest topology that makes `f`

continuous.

## Equations

## Instances For

## Equations

- instTopologicalSpaceSubtype = TopologicalSpace.induced Subtype.val t

Given `f : X → Y`

and a topology on `X`

,
the coinduced topology on `Y`

is defined such that
`s : Set Y`

is open if the preimage of `s`

is open.
This is the finest topology that makes `f`

continuous.

## Equations

- TopologicalSpace.coinduced f t = { IsOpen := fun (s : Set Y) => IsOpen (f ⁻¹' s), isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

## Instances For

We say that restrictions of the topology on `X`

to sets from a family `S`

generates the original topology,
if either of the following equivalent conditions hold:

- a set which is relatively open in each
`s ∈ S`

is open; - a set which is relatively closed in each
`s ∈ S`

is closed; - for any topological space
`Y`

, a function`f : X → Y`

is continuous provided that it is continuous on each`s ∈ S`

.

## Instances For

A function `f : X → Y`

between topological spaces is inducing if the topology on `X`

is induced
by the topology on `Y`

through `f`

, meaning that a set `s : Set X`

is open iff it is the preimage
under `f`

of some open set `t : Set Y`

.

- induced : tX = TopologicalSpace.induced f tY
The topology on the domain is equal to the induced topology.

## Instances For

The topology on the domain is equal to the induced topology.

A function between topological spaces is an embedding if it is injective,
and for all `s : Set X`

, `s`

is open iff it is the preimage of an open set.

- induced : inst✝¹ = TopologicalSpace.induced f inst✝
- inj : Function.Injective f
A topological embedding is injective.

## Instances For

A topological embedding is injective.

An open embedding is an embedding with open range.

- induced : tX = TopologicalSpace.induced f tY
- inj : Function.Injective f
The range of an open embedding is an open set.

## Instances For

The range of an open embedding is an open set.

A closed embedding is an embedding with closed image.

- induced : tX = TopologicalSpace.induced f tY
- inj : Function.Injective f
The range of a closed embedding is a closed set.

## Instances For

The range of a closed embedding is a closed set.

A function between topological spaces is a quotient map if it is surjective,
and for all `s : Set Y`

, `s`

is open iff its preimage is an open set.

## Equations

- QuotientMap f = (Function.Surjective f ∧ tY = TopologicalSpace.coinduced f tX)