NYLL
Module

CoefficientPullback.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.CoefficientPullback
5 declarations indexed from sourceView source ↗

Module documentation

Coefficient base change of charts and overlaps

The literal pullbacks of two charts along a coefficient map form a cartesian overlap. The comparison with their fiber product preserves both chart projections.

Imports2
  • Mathlib.AlgebraicGeometry.Pullbacks
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Imported by2

Declarations

theorem

coefficientBaseChange_isPullback

L39 ↗
EtaleFundamentalGroups.coefficientBaseChange_isPullback
Documentation

The literal base-change map and second projections form a cartesian square.

Source context 10 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S A B : Scheme.{u}} (φ : T' ⟶ T) (f : S ⟶ T) (a : A ⟶ S) (b : B ⟶ S)
local notation "v" => (pullback.fst a b ≫ a ≫ f)
local notation "aL" =>
  (pullback.lift (pullback.fst φ (a ≫ f)) (pullback.snd φ (a ≫ f) ≫ a)
    (Eq.trans pullback.condition (Eq.symm (Category.assoc _ _ _))))
local notation "bL" =>
  (pullback.lift (pullback.fst φ (b ≫ f)) (pullback.snd φ (b ≫ f) ≫ b)
    (Eq.trans pullback.condition (Eq.symm (Category.assoc _ _ _))))
local notation "α" =>
  (pullback.lift (pullback.fst φ v) (pullback.snd φ v ≫ pullback.fst a b)
    (Eq.trans pullback.condition (Eq.symm (Category.assoc _ _ _))))
local notation "β" =>
  (pullback.lift (pullback.fst φ v) (pullback.snd φ v ≫ pullback.snd a b)
    (Eq.trans pullback.condition (Eq.trans (congrArg (fun h ↦ pullback.snd φ v ≫ h)
      (pullback.condition_assoc f)) (Eq.symm (Category.assoc _ _ _)))))
Lean source · statement
theorem coefficientBaseChange_isPullback :
    IsPullback aL (pullback.snd φ (a ≫ f)) (pullback.snd φ f) a
theorem

coefficientPullback_isPullback

L46 ↗
EtaleFundamentalGroups.coefficientPullback_isPullback
Documentation

Pulling back a fiber product along the coefficient base change remains a fiber product of the literal base-changed factors.

Source context 10 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S A B : Scheme.{u}} (φ : T' ⟶ T) (f : S ⟶ T) (a : A ⟶ S) (b : B ⟶ S)
local notation "v" => (pullback.fst a b ≫ a ≫ f)
local notation "aL" =>
  (pullback.lift (pullback.fst φ (a ≫ f)) (pullback.snd φ (a ≫ f) ≫ a)
    (Eq.trans pullback.condition (Eq.symm (Category.assoc _ _ _))))
local notation "bL" =>
  (pullback.lift (pullback.fst φ (b ≫ f)) (pullback.snd φ (b ≫ f) ≫ b)
    (Eq.trans pullback.condition (Eq.symm (Category.assoc _ _ _))))
local notation "α" =>
  (pullback.lift (pullback.fst φ v) (pullback.snd φ v ≫ pullback.fst a b)
    (Eq.trans pullback.condition (Eq.symm (Category.assoc _ _ _))))
local notation "β" =>
  (pullback.lift (pullback.fst φ v) (pullback.snd φ v ≫ pullback.snd a b)
    (Eq.trans pullback.condition (Eq.trans (congrArg (fun h ↦ pullback.snd φ v ≫ h)
      (pullback.condition_assoc f)) (Eq.symm (Category.assoc _ _ _)))))
Lean source · statement
theorem coefficientPullback_isPullback : IsPullback α β aL bL
def

coefficientPullbackIso

L61 ↗
EtaleFundamentalGroups.coefficientPullbackIso
Documentation

The actual comparison of base-changed overlaps with overlaps of base-changed factors.

Source context 10 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S A B : Scheme.{u}} (φ : T' ⟶ T) (f : S ⟶ T) (a : A ⟶ S) (b : B ⟶ S)
local notation "v" => (pullback.fst a b ≫ a ≫ f)
local notation "aL" =>
  (pullback.lift (pullback.fst φ (a ≫ f)) (pullback.snd φ (a ≫ f) ≫ a)
    (Eq.trans pullback.condition (Eq.symm (Category.assoc _ _ _))))
local notation "bL" =>
  (pullback.lift (pullback.fst φ (b ≫ f)) (pullback.snd φ (b ≫ f) ≫ b)
    (Eq.trans pullback.condition (Eq.symm (Category.assoc _ _ _))))
local notation "α" =>
  (pullback.lift (pullback.fst φ v) (pullback.snd φ v ≫ pullback.fst a b)
    (Eq.trans pullback.condition (Eq.symm (Category.assoc _ _ _))))
local notation "β" =>
  (pullback.lift (pullback.fst φ v) (pullback.snd φ v ≫ pullback.snd a b)
    (Eq.trans pullback.condition (Eq.trans (congrArg (fun h ↦ pullback.snd φ v ≫ h)
      (pullback.condition_assoc f)) (Eq.symm (Category.assoc _ _ _)))))
Lean source · statement
def coefficientPullbackIso : pullback φ v ≅ pullback aL bL
theorem

coefficientPullbackIso_hom_fst

L65 ↗
EtaleFundamentalGroups.coefficientPullbackIso_hom_fst
Documentation

The comparison has the canonical projection to the first base-changed factor.

Source context 10 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S A B : Scheme.{u}} (φ : T' ⟶ T) (f : S ⟶ T) (a : A ⟶ S) (b : B ⟶ S)
local notation "v" => (pullback.fst a b ≫ a ≫ f)
local notation "aL" =>
  (pullback.lift (pullback.fst φ (a ≫ f)) (pullback.snd φ (a ≫ f) ≫ a)
    (Eq.trans pullback.condition (Eq.symm (Category.assoc _ _ _))))
local notation "bL" =>
  (pullback.lift (pullback.fst φ (b ≫ f)) (pullback.snd φ (b ≫ f) ≫ b)
    (Eq.trans pullback.condition (Eq.symm (Category.assoc _ _ _))))
local notation "α" =>
  (pullback.lift (pullback.fst φ v) (pullback.snd φ v ≫ pullback.fst a b)
    (Eq.trans pullback.condition (Eq.symm (Category.assoc _ _ _))))
local notation "β" =>
  (pullback.lift (pullback.fst φ v) (pullback.snd φ v ≫ pullback.snd a b)
    (Eq.trans pullback.condition (Eq.trans (congrArg (fun h ↦ pullback.snd φ v ≫ h)
      (pullback.condition_assoc f)) (Eq.symm (Category.assoc _ _ _)))))
Lean source · statement
theorem coefficientPullbackIso_hom_fst :
    (coefficientPullbackIso φ f a b).hom ≫ pullback.fst aL bL = α
theorem

coefficientPullbackIso_hom_snd

L70 ↗
EtaleFundamentalGroups.coefficientPullbackIso_hom_snd
Documentation

The comparison has the canonical projection to the second base-changed factor.

Source context 10 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {T T' S A B : Scheme.{u}} (φ : T' ⟶ T) (f : S ⟶ T) (a : A ⟶ S) (b : B ⟶ S)
local notation "v" => (pullback.fst a b ≫ a ≫ f)
local notation "aL" =>
  (pullback.lift (pullback.fst φ (a ≫ f)) (pullback.snd φ (a ≫ f) ≫ a)
    (Eq.trans pullback.condition (Eq.symm (Category.assoc _ _ _))))
local notation "bL" =>
  (pullback.lift (pullback.fst φ (b ≫ f)) (pullback.snd φ (b ≫ f) ≫ b)
    (Eq.trans pullback.condition (Eq.symm (Category.assoc _ _ _))))
local notation "α" =>
  (pullback.lift (pullback.fst φ v) (pullback.snd φ v ≫ pullback.fst a b)
    (Eq.trans pullback.condition (Eq.symm (Category.assoc _ _ _))))
local notation "β" =>
  (pullback.lift (pullback.fst φ v) (pullback.snd φ v ≫ pullback.snd a b)
    (Eq.trans pullback.condition (Eq.trans (congrArg (fun h ↦ pullback.snd φ v ≫ h)
      (pullback.condition_assoc f)) (Eq.symm (Category.assoc _ _ _)))))
Lean source · statement
theorem coefficientPullbackIso_hom_snd :
    (coefficientPullbackIso φ f a b).hom ≫ pullback.snd aL bL = β

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