NYLL
Module

CommAlgInertiaRingMaps.lean

Nyll.EtaleFundamentalGroups.Inertia.CommAlgInertiaRingMaps
2 declarations indexed from sourceView source ↗

Module documentation

Ring maps underlying intrinsic inertia

Extracts the coefficient ring map of an intrinsic inertia element and proves that this ring map determines the element.

Imports3
Imported by6

Declarations

def

commAlgIdealInertiaRingHom

L23 ↗
EtaleFundamentalGroups.Inertia.commAlgIdealInertiaRingHom
Documentation

An intrinsic inertia element's literal coefficient ring map.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Inertia
universe u v
Lean source · statement
def commAlgIdealInertiaRingHom
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A) (Q : Ideal B)
    (σ : commAlgIdealInertiaGroup A B Q) : B →+* B
theorem

commAlgIdealInertiaRingHom_injective

L29 ↗
EtaleFundamentalGroups.Inertia.commAlgIdealInertiaRingHom_injective
Documentation

The literal coefficient map determines the intrinsic inertia element.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Inertia
universe u v
Lean source · statement
theorem commAlgIdealInertiaRingHom_injective
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A) (Q : Ideal B) :
    Function.Injective (commAlgIdealInertiaRingHom A B Q)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.