NYLL
Module

CanonicalPointedComposition.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.CanonicalPointedComposition
3 declarations indexed from sourceView source ↗

Module documentation

Strict composition with the canonical geometric-point identifications

The pullback pentagon identifies the composite fiber comparison with the canonical one. Consequently the original fundamental-group homomorphisms compose after transport along the specified equality of geometric points.

Imports1
Imported by5

Declarations

theorem

pullbackFiberIso_transport_hom_app

L33 ↗
AlgebraicGeometry.FiniteEtale.pullbackFiberIso_transport_hom_app
Documentation

A fiber comparison transported to an equal point is the inverse of the actual pullback-composition comparison with that specified composite.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.Functor CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
variable {X Y Z : Scheme.{u}} {Ω : Type u} [Field Ω]
Lean source · statement
theorem pullbackFiberIso_transport_hom_app
    (f : X ⟶ Y) (point : Spec (.of Ω) ⟶ X) (eta : Spec (.of Ω) ⟶ Y)
    (heta : point ≫ f = eta) (A : FiniteEtale Y) :
    (pullbackFiberIso f point ≪≫ eqToIso (congrArg fiber heta)).hom.app A =
      (forgetScheme Ω).map
        ((MorphismProperty.Over.pullbackComp
          (P := @IsFiniteEtale) (Q := ⊤) point f eta heta.symm).inv.app A)
theorem

pullbackCompositeFiberIsoOfEq_eq_pullbackFiberIso

L50 ↗
AlgebraicGeometry.FiniteEtale.pullbackCompositeFiberIsoOfEq_eq_pullbackFiberIso
Documentation

The composite canonical comparison is the canonical comparison for the composite scheme map, with its prescribed equality of target points.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.Functor CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
variable {X Y Z : Scheme.{u}} {Ω : Type u} [Field Ω]
Lean source · statement
theorem pullbackCompositeFiberIsoOfEq_eq_pullbackFiberIso
    (f : X ⟶ Y) (g : Y ⟶ Z) (m : X ⟶ Z) (hm : m = f ≫ g)
    (point : Spec (.of Ω) ⟶ X) (hpoint : (point ≫ f) ≫ g = point ≫ m) :
    pullbackCompositeFiberIsoOfEq f g m hm point (point ≫ m) hpoint = pullbackFiberIso m point
theorem

fundamentalGroupHom_comp_of_eq

L110 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_comp_of_eq
Documentation

The original fundamental-group maps compose strictly after the prescribed transport of the target geometric point.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.Functor CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
variable {X Y Z : Scheme.{u}} {Ω : Type u} [Field Ω]
Lean source · statement
theorem fundamentalGroupHom_comp_of_eq
    (f : X ⟶ Y) (g : Y ⟶ Z) (m : X ⟶ Z) (hm : m = f ≫ g)
    (point : Spec (.of Ω) ⟶ X) (hpoint : (point ≫ f) ≫ g = point ≫ m)
    (a : π₁ᵉᵗ(point)) :
    hpoint ▸ fundamentalGroupHom g (point ≫ f) (fundamentalGroupHom f point a) =
      fundamentalGroupHom m point a

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