Module

PointedQuotientTransport.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.PointedQuotientTransport

3 declarations indexed from sourceView source ↗

Module documentation

Transport of pointed Galois quotients

The quotient attached to a Galois object is natural under an isomorphism between fiber functors, provided that the chosen point is transported along the same isomorphism.

Imports3

Nyll.EtaleFundamentalGroups.GaloisCategories.GaloisObjectQuotient
Nyll.EtaleFundamentalGroups.GaloisCovers.FiberQuotient
Mathlib.CategoryTheory.Conj

Imported by4

theorem

galoisObjectQuotientMonoidHom_transport

L32 ↗

CategoryTheory.PreGaloisCategory.galoisObjectQuotientMonoidHom_transport

Documentation

Pointed Galois-object quotients commute with conjugation along an isomorphism of fiber functors.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u₁ u₂ w
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable (Phi Psi : C ⥤ FintypeCat.{w}) [FiberFunctor Phi] [FiberFunctor Psi]

Lean source · statement

theorem galoisObjectQuotientMonoidHom_transport
    (p : Phi ≅ Psi) (A : C) [IsGalois A]
    (y : Psi.obj A) (a : Aut Phi) :
    galoisObjectQuotientMonoidHom Phi (Aut Phi) A (p.inv.app A y) a =
      galoisObjectQuotientMonoidHom Psi (Aut Psi) A y (p.conjAut a)

theorem

galoisObjectQuotientMonoidHom_transport_comp

L62 ↗

CategoryTheory.PreGaloisCategory.galoisObjectQuotientMonoidHom_transport_comp

Documentation

Naturality of pointed Galois-object quotients after precomposition by an arbitrary group homomorphism.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u₁ u₂ w
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable (Phi Psi : C ⥤ FintypeCat.{w}) [FiberFunctor Phi] [FiberFunctor Psi]

Lean source · statement

theorem galoisObjectQuotientMonoidHom_transport_comp
    (p : Phi ≅ Psi) (A : C) [IsGalois A]
    (y : Psi.obj A) {G : Type*} [Group G]
    (h : G →* Aut Phi) :
    (galoisObjectQuotientMonoidHom
        Phi (Aut Phi) A (p.inv.app A y)).comp h =
      (galoisObjectQuotientMonoidHom Psi (Aut Psi) A y).comp
        (p.conjAut.toMonoidHom.comp h)

theorem

finiteEtaleGaloisCoverQuotientMonoidHom_transport

L85 ↗

EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientMonoidHom_transport

Documentation

Finite-etale specialization of pointed-quotient transport.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem finiteEtaleGaloisCoverQuotientMonoidHom_transport
    {X : Scheme.{u}} [ConnectedSpace X]
    {Omega Omega' : Type u}
    [Field Omega] [IsSepClosed Omega]
    [Field Omega'] [IsSepClosed Omega']
    (xi : Spec (.of Omega) ⟶ X) (xi' : Spec (.of Omega') ⟶ X)
    (p : fiber xi ≅ fiber xi')
    (Y : FiniteEtale X) (hY : IsGalois Y)
    (y : (fiber xi').obj Y) (a : Aut (fiber xi)) :
    finiteEtaleGaloisCoverQuotientMonoidHom
        xi Y hY (p.inv.app Y y) a =
      finiteEtaleGaloisCoverQuotientMonoidHom
        xi' Y hY y (p.conjAut a)

Module documentation

Transport of pointed Galois quotients

Declarations

galoisObjectQuotientMonoidHom_transport

galoisObjectQuotientMonoidHom_transport_comp

finiteEtaleGaloisCoverQuotientMonoidHom_transport