NYLL
Module

AlgHomReconstruction.lean

Nyll.EtaleFundamentalGroups.Purity.HeightOne.AlgHomReconstruction
2 declarations indexed from sourceView source ↗

Module documentation

Reconstructing algebra morphisms after linear descent

Codimension-one intersection arguments naturally descend a generic-fibre linear map before they establish its multiplicative structure. If the descended map becomes an algebra morphism after composition with an injective algebra map, preservation of one and multiplication reflects back to the original target. This file packages that reconstruction step.

Imports1
Imported by1

Declarations

theorem

existsUnique_algHom_of_comp_eq_of_injective

L27 ↗
EtaleFundamentalGroups.existsUnique_algHom_of_comp_eq_of_injective
Documentation

A linear map which becomes an algebra morphism after composition with an injective algebra map underlies a unique algebra morphism.

Source context 3 commands

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

namespace EtaleFundamentalGroups
universe u v w z
noncomputable section
Lean source · statement
theorem existsUnique_algHom_of_comp_eq_of_injective
    {R : Type u} {S : Type v} {T : Type w} {U : Type z}
    [CommSemiring R] [Semiring S] [Semiring T] [Semiring U]
    [Algebra R S] [Algebra R T] [Algebra R U]
    (g : S →ₗ[R] T) (ι : T →ₐ[R] U) (hι : Function.Injective ι)
    (f : S →ₐ[R] U) (hcomp : ι.toLinearMap.comp g = f.toLinearMap) :
    ∃! φ : S →ₐ[R] T, φ.toLinearMap = g
theorem

existsUnique_algEquiv_of_comp_eq_of_injective

L62 ↗
EtaleFundamentalGroups.existsUnique_algEquiv_of_comp_eq_of_injective
Documentation

A linear equivalence which becomes an algebra morphism after composition with an injective algebra map underlies a unique algebra equivalence.

Source context 3 commands

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

namespace EtaleFundamentalGroups
universe u v w z
noncomputable section
Lean source · statement
theorem existsUnique_algEquiv_of_comp_eq_of_injective
    {R : Type u} {S : Type v} {T : Type w} {U : Type z}
    [CommSemiring R] [Semiring S] [Semiring T] [Semiring U]
    [Algebra R S] [Algebra R T] [Algebra R U]
    (e : S ≃ₗ[R] T) (ι : T →ₐ[R] U) (hι : Function.Injective ι)
    (f : S →ₐ[R] U)
    (hcomp : ι.toLinearMap.comp e.toLinearMap = f.toLinearMap) :
    ∃! φ : S ≃ₐ[R] T, φ.toLinearEquiv = e

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