Theorems · Definition · algebraic geometry
CommAlgCat.FiniteEtale.fiber
(R : Type u) →
[inst : CommRing R] →
(Ω : Type w) → [inst_1 : Field Ω] → [Algebra R Ω] → CategoryTheory.Functor (CommAlgCat.FiniteEtale R)ᵒᵖ FintypeCatThe fiber functor for finite étale R-algebras at the geometric point Ω: This is the
functor sending S to R-algebra homomorphisms S →ₐ[R] Ω.
- Defined in
- Mathlib.RingTheory.Etale.Finite
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- CommRingstatement and proof · cited by 17,173
- CategoryTheory.Functorstatement · cited by 16,252
- Algebrastatement and proof · cited by 11,388
- Oppositestatement and proof · cited by 8,081
- Fieldstatement and proof · cited by 7,404
- AlgHomproof · cited by 3,236
- Finitestatement · cited by 3,029
- Opposite.unopproof · cited by 2,231
- CategoryTheory.ObjectProperty.FullSubcategory.objproof · cited by 1,316
- Quiver.Hom.unopproof · cited by 903
- CategoryTheory.InducedCategory.Hom.homproof · cited by 850
Cited by5
Results whose statement or proof uses this declaration.
- CommAlgCat.FiniteEtale.fiberIsoCompstatement · cited by 0
- CommAlgCat.FiniteEtale.fiberIsoFiniteSpecstatement · cited by 0
- CommAlgCat.FiniteEtale.fiber_mapstatement and proof · cited by 0
- CommAlgCat.FiniteEtale.fiber_obj_objstatement and proof · cited by 0
- CommAlgCat.FiniteEtale.fiberIsoBaseChangeFiberstatement · cited by 0