AlgebraicGeometry.FiniteEtale.exists_nontrivial_deck_of_iso_square
A proved isomorphism square transports a nonidentity actual deck transformation to a nonidentity actual deck transformation.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry.FiniteEtaleLean source · statement
theorem exists_nontrivial_deck_of_iso_square
{X Y X' Y' : Scheme}
(eX : X ≅ X') (eY : Y ≅ Y')
(f : X ⟶ Y) (g : X' ⟶ Y')
[IsFiniteEtale f] [IsFiniteEtale g]
(hfg : f ≫ eY.hom = eX.hom ≫ g)
(σ : Aut (FiniteEtale.mk g)) (hσ : σ ≠ 1) :
∃ ρ : Aut (FiniteEtale.mk f), ρ ≠ 1